[Cryptography] The Case for Formal Verification

[Derek Jones]

Tim,

> With all due respect, most of the points you make are ridiculous.

Could you please explain why you think they are ridiculous.

> For example, you point out that the certified C compiler will not
> make any guarantees about code that relies on undefined behavior.
> Well, of course! Being certified doesn't magically fix your specification!
> Certified just says the implementation matches the specification!

Where did the word "certified" come from?  I have not said anything
about magically fixing a specification.

The CompCert people are claiming a formally verified compiler and I
think this claim is very misleading to say the least.

> And to suggest that such a project is misguided because it places
> blind trust in coq (and because it is written in ocaml?!) shows a

I did not say that this project was misguided.

> misunderstanding of the proof tools. There is a very small core of
> trust that you need to have faith in and it is backed by solid theory

Yes, the axioms.  These need to be small in number and 'obviously'
correct; something that cannot be said of the source code of coq.
The nearest I can think of is the Lisp subset written in itself in
under a 100 lines (my memory is vague on this point)

> and is a much more solid foundation for building on than just about
> any other software we have in computer science. I don't see how in
> any way you can compare the f2c translator to this effort.

Why not?  What work has been done on the coq+other tools that has not
been done on f2c?

I describe work that was done to try and show the correctness of
a Model Implementation for C here:
http://shape-of-code.coding-guidelines.com/2011/05/02/estimating-the-quality-of-a-compiler-implemented-in-mathematics/

[ My original post to this list bounced, so I am reposting it here now), it
cam ebefore the message it is replying to]