Re: Reinterpreting the compiler source code

[Richard Stallman <rms@gnu.org>]

[[[ 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.