[[[ To any NSA and FBI agents reading my email: please consider ]]] [[[ whether defending the US Constitution against all enemies, ]]] [[[ foreign or domestic, requires you to follow Snowden's example. ]]]
I can speak in favor of any serious effort to try to verify that our binaries match our souce code. > What we need is a language with a simple semantics for which we can write > interpreters from scratch. It will be slow, but that doesn't matter. All we > need it for is to generate the reference compiler that we know is secure, > and the reference tools that we use to verify that the object code produced > by the full 740 MB of GCC source when compiled by the 74MB gcc binaries, is > the same object code our reference compiler produces. I did not understand, until now, that this was meant as a way to verify GCC. I thought you meant we should stop using our existing tools and program in this language instead. I was not interested in that. However, as a scheme to verify our tools and keep using them, it might make sense. I can't judge how effective this sort of proof might be, but I won't reject the idea. -- Dr Richard Stallman President, Free Software Foundation 51 Franklin St Boston MA 02110 USA www.fsf.org www.gnu.org Skype: No way! That's nonfree (freedom-denying) software. Use Ekiga or an ordinary phone call.
