Re: Bug free programs

[Mark H Weaver <mhw@netris.org>]

Hi Ian,

I'm going to try to ignore your gratutious and unfounded insults,
because I agree that the problem you are trying to solve is an important
one, and believe it or not, you'd be hard pressed to find anyone else in
the GNU project who worries about this issue as much as I do.

For example, on an internal GNU mailing list, I complained when GCC
switched to using C++ because it vastly increases the complexity of the
simplest compiler that's able to bootstrap it.

The reason is that for a few years now, I've very seriously considered
dedicating myself to developing a bootstrap procedure that starts with
raw machine code running on bare metal and ends with a working GNU
toolchain.

I've also considered more practical approaches such as: lock a
(preferably older) computer inside a Faraday cage to prevent
communication with the outside world, thus limiting the intelligence
that any Thompson virus can have, while I write a very simple and novel
C compiler that's capable of bootstrapping GCC and the rest of the
toolchain, and then printing the result to paper in a form that can be
scanned reliably -- a task I have some experience with, since I led the
development of the scannable PGP source code books that allowed PGP to
be legally exported from the US fo the first time, along with the tools
needed to convert the paper books back into electronic form with modest
effort.

Ian Grant <ian.a.n.grant@googlemail.com> writes:

> On Tue, Sep 16, 2014 at 11:27 PM, Mark H Weaver <mhw@netris.org>
> wrote:
>
>     Ian Grant <ian.a.n.grant@googlemail.com> writes:
>     
>     Are you suggesting that we compile our Scheme code to C, include
>     that
>     in our distribution, and then users would start by compiling that
>     (non-source) C code? If so, I'm surprised to hear you suggest
>     that,
>     given your concern over Thompson viruses (which I share,
>     incidentally).
>     A Thompson virus could be hiding in this intermediate C code that
>     would
>     be very hard to audit.
>
> Tell me, how did you compile your OS kernel and your glibc, ld.so, ld,
> as and gcc binaries? 

Yes, that's a very serious problem, but I don't want to make the problem
worse by adding yet another pile of intermediate C code that must be
taken on faith to be free of Thompson viruses.

>     I, for one, am very glad that unlike many self-hosting compilers,
>     Guile
>     is bootstrapped entirely from source code, with just one
>     exception:
>     psyntax-pp.scm is generated from psyntax.scm, but it's fairly
>     close to
>     the source code and quite readable. Incidentally, I put a great
>     deal of
>     effort into making sure it was readable.
>
> I can assure you that Guile is most certainly not bootstrapped
> entirely from source code. If you had understood any of the discussion
> about the problem you would know that there is not one single line of
> GNU source that has ever been bootstrapped from source code.

I understand that just fine.  It's obvious that to compile Guile, you
first need a C toolchain.  That's a separate problem, and indeed a very
serious one.

>     > See the thunder.pdf I sent when I first proposed this idea:
>     >
>     >
>     http://lists.gnu.org/archive/html/guile-devel/2014-08/msg00064.html
>     
>     If you want me to read it, can you please email it as plain text?
>
> No: because If you can't read a PDF then you can't read _any_ of the
> research papers you need to be able to read in order to stand the
> slightest chance of doing a decent job of developing any kind of
> software at all.

Wow.  Did you try telling that to RMS, who made the same suggestion?

I read plenty of PDFs.  They are inconvenient, but I suffer that
inconvenience on a regular basis, when I have reason to believe that I
might learn something new from them.  So far, not a single person has
recommended your paper to me except you, nor have I learned anything I
didn't already know from the emails you've written, at least not from
the prefixes of those emails that I've read before losing interest.

I'm not saying that you don't have something to teach me.  Maybe you do,
but if so, you must learn the art of capturing the interest of your
readers long enough to convince them that they should continue reading.

At present, you're in the position of having to convince me that you're
ideas are worth studying, not the other way around, and I suspect I'm
not alone.  It would help to tell me something I didn't already know, in
ASCII, as concisely as possible.

      Mark