FOM: Program verification

[Andrej Bauer]

Andrzej Trybulec <trybulec at math.uwb.edu.pl> writes:

> The goal of program verification is not to guarantee that the program is
> correct, but to find bugs, and the to make a program a bit more reliable.
> 
> And it seems that most of programs have bugs. If not all.

Thanks for raising this extremely important point. The goal of program
verification and of programming language design is NOT to make perfect
programs, but to make BETTER programs. I think this may not be
entirely clear around here.

In practice the primary result of program verification (or a good type
system--which is a form of verification) is that it catches a whole
lot of silly little bugs that were introduced by programmers. That's
the main gain. The secondary gain is to detect design errors in
algorithms, communication protocols, etc.

In practice it is extremely useful even to just partially verify a
program, i.e., in an unrealistic model of computation that only
captures certain aspects of the real world. Snubbing program
verification on the grounds that it is somehow an inferior form of
"proof" is not only silly but also mistaken.

> Of course I have some ulterior motives:
> I heard an opinion, not once, that program verification is the most
> important (the only important) challenge for mathematics in this century
> and if mathematicians fail, the government should stop cut all money for
> mathematics. And I would like to get my salary.

Move to a CS department...

I've heard more than once comments that mathematicians are losing
prospective graduate students to their colleagues from computer
science departments. Is this true? Are the bright students choosing
computer science departments over math departments? Is it just money,
or has the interesting math moved to CS departments?

--
Andrej Bauer
http://andrej.com