[Cryptography] Ada vs Rust vs safer C

[Peter Gutmann]

Jerry Leichter <leichter at lrw.com> writes:

>This was based on a very expressive annotation language and a fairly powerful
>proof engine, so with proper annotations you could verify some quite
>meaningful properties of C (or other language) programs.  Unfortunately, the
>annotation language was highly mathematical in form, well beyond the comfort
>zone (or even competence) of the vast majority of programmers.  So the effort
>never had any significant real-world impact.

There have been several projects like this, e.g. Larch and LCLint/splint,
which required near-incomprehensible annotations and produced near-
incomprehensible diagnostics.  It requires experts to use, and another set of
experts to evaluate the results.

The problem with all of these is that the designers chose to create a
metalanguage/system for specifying the precise semantics of a program, which
means you need to create a second copy of your code using mathematical
notation, and the proof assistant then checks whether your mathematical
description matches what your code does.  The problems with this are that most
coders prefer to only write their code once, the notation is invariably near-
incomprehensible, it often can't express what the developers are trying to do
(by long-standing tradition you demonstrate it using toy examples like a
simple quicksort, or even just a memcpy()), and the developers are looking for
a tool that gives them something like what a Pascal compiler would do, not a
full-blown formal verification system.

>This is the side of annotations and program verification systems that's
>proved a stumbling block pretty much forever.  No one has really solved the
>problem of working either with un-annotated code in languages that are in
>actual use; or designing an annotation system that real-world programmers can
>use effectively.

PREfast does a pretty good job.  What made the PREfast work unique is that
they didn't start with some abstract mathematical goal (well, not once they
got the tool into production use beyond the research stage) but looked at what
real-world programmers were doing and created what was needed to deal with
that.  It's evolved continuously over the years to match real-world
experience, so the current SAL and PREfast is very different from what it was
five and ten years ago.

Peter.