Robert Dewar <[EMAIL PROTECTED]> writes: | Gabriel Dos Reis wrote: | | > C is | > trustworthy (and preferred over SML for that curcial part of the proof | > checker) because the mapping of the C code to the generated assembly | > code is straighforward and amenable to inspection. | | This kind of traceability is of course vital for such applications, but | it is by no means unique to C,
Nobody claims it is unique to C. You're after the wrong target. | and there is a big difference between saying | that C is an assembly language, and that the mapping of C to assembly | language is transparent. Oh, you denied any connection in previous message. -- Gaby