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, 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. The latter quality incidentally, Tucker Taft describes as WYSIWYG for programming languages, and it is an important design point for C I would say, and indeed was an important design principle for Ada.
