[cap-talk] Confessions of a C programmer

[Matej Kosik]

Bill Frantz wrote:
> daw at cs.berkeley.edu (David Wagner) on Tuesday, September 22, 2009 wrote:
> 
>> Bill Frantz  wrote:
>>> Languages with a run-time interpreter, such as Java, have the issue of
>>> verifying what is usually a fairly large C program.
>> On the other hand, compiled languages have the issue of verifying what
>> is usually a fairly large program (the compiler).  I'm not sure there is
>> necessarily a big win for compiled languages over interpreted languages.
>> Either way, you are relying on the compiler/interpreter and the associated
>> runtime libraries and related infrastructure.  It's pretty rare to see
>> those formally verified, no matter what language you use, so in practice
>> almost any language involves relying upon a large, unverified program.
>> (Now there might be reasons why that program is more trustworthy in
>> some cases than others, to be sure.)
> 
> (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.

Quite interesting related result:

http://compcert.inria.fr

If something can be called science (as opposed to spreading patascience)
then I guess this is it.

If I understand this result correstly, with respect to TCB size, if we
use this compiler, it is outside TCB. Its specification is what has to
concern us because the specification (not the proof) belongs to TCB.

But regression continues. Coq is then part of TCB. Oh well. :(
-- 
Matej Kosik