[cap-talk] Confessions of a C programmer

[David Wagner]

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.)