[cap-talk] Confessions of a C programmer

[Ben Kloosterman]

>(Hehe) And probably the easiest "compiler" to verify is an assembler,
>since
>the output is directly related to the input. Of course you lose
>portability
>and memory safety, although Norm wrote some ideas for verifying machine
>code in <http://cap-lore.com/Software/CodeProof/>.
>
>If one could verify some useful static properties of machine code, and
>run
>the verifier in a way that it could not modify the code being verified,
>you
>might end up with smallest development system to verify. Just a thought.

This is exactly why Singularity et al. uses CIL as an Intermediate language,
the compiler is not much more  than an assembler ( with some basic
optimization like inlining) and you still get multi platform support.
Verifying a C or C++ compiler is a very arduous task. Verifying a kernel and
a CIL assembler/compiler is possible. 

If you want a language that helps with verifying have you looked at Spec#/
Sing# and the Boogie verification engine ? 
Towards a Verifying Compiler: The Spec# Approach:
http://research.microsoft.com/en-us/projects/specsharp/fm-schulte-lecture1.p
pt ( there are 4 follow ons)  (A tutorial presented at Marktoberdorf 2006
and FM 2006).




Regards, 

Ben