Georg Bauhaus <[EMAIL PROTECTED]> writes: | Gabriel Dos Reis wrote: | > Robert Dewar <[EMAIL PROTECTED]> writes: | > | Gabriel Dos Reis wrote: | > | | But the whole idea of hardware semantics is bogus, since you are | > | assuming some connection between C and the hardware which does not | > | exist. C is not an assembly language. | > If you live in a different world, you may not see the connection. | | I'm not sure whether this isn't just C's self-fulfilling | prophecy at work: Many C programmers think that C is a high level
self-fulfilling prophecy or not, would you deny that processor specific ABIs are published and programmers expect compilers to follow them? GCC itself relies on such connection. | assembly language (at least in my real world). | They start using C as if it were... Well, I would not say it is something unique to C programmers. Recently we had a guest working on compiler verification and model checking, deeply rooted in the ML community explain us the architecture of their proof checker. The heart of the proof checker, the trusted part, is written in C instead of SML. When the question was asked as to why -- probably because people were surprised, given their close tie to SML -- and the answer was simple: even though it can be claimed that the C type system is unsound and SML's is sound, 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. -- Gaby