In comparison to generating a proof, verifying a proof is an easy
problem to mechanize.
> Type validation is useful, but only when the types themselves prevent
> invalid accesses. C types don't insure that you can't write past the limits
> of the typed address range (scalar variable, structure, array, etc.), so it
> doesn't accomplish anything useful in practice.
It's worse than that. In general, "Safe" execution of C programs
simply cannot be proved (for some useful definition of safe). And if
it was possible to prove the relevant properties for realistic
programs (despite the "in general" disclaimer), I think compiler
writers would have noticed it by now, giving that they've been looking
at this kind of problem for a few decades.
For languages like Java, the type system doesn't just make it easy to
prove the relevant properties - it actually constrains the language so
that for well-typed programs the relevant properties hold (proving
this last bit is tough in itself, but can be done, because the proof
is done for the definition of a particular language, rather than "in
general").
-- Dave Wragg- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.rutgers.edu Please read the FAQ at http://www.tux.org/lkml/faq.html