SPARK

poormattie pointed me at SPARK. It's a commercial programming language and toolset for making extremely reliable programs. The idea is that testing isn't good enough: you need to prove your program correct.

Here's how to construct the SPARK language. (I am not 100% sure on all the details; this is from reading the SPARK web site, which contains no code examples.)

1. Start with Ada. In fact all SPARK programs are Ada programs, and you can use whatever Ada compiler you like to compile them.
2. Remove all the interesting features (threading, allocating objects with new, exceptions, generics, even recursion). I speculate that by doing this you have already achieved 80% of the reliability improvement you're going to get. You've effectively discouraged programmers from taking any mental shortcuts whatsoever or doing anything hard.
3. Add an annotation language for preconditions, postconditions, and assertions. The annotations go in Ada comments, so your Ada compiler will ignore them.
4. Add a separate file format (outside your source files) for machine-verifiable proofs. You might want to prove, for example, that a given assert will always be true, if the preconditions and invariants are met; that all methods of a class preserve the class invariants; that a procedure always terminates; that a given array index is always in the right range; that a given call to a function always passes parameters that meet its preconditions; etc.

You can buy a static analysis tool that checks your code and makes sure it's SPARK language (i.e. that you're not using any Ada features that SPARK forbids). Then you can buy a proof assistant that helps you write proofs. Presumably one of these tools also verifies proofs and tells you how much of your program is actually covered by your proofs. (For example, your development project might institute a policy that every assertion needs to be proved, and every array access needs to be proved in-bounds; the tool presumably tells you when you've done this and what's missing.)

There is a definite appeal to this kind of tool for some projects, and the notion that test-driven development is horribly misguided makes me smile. But SPARK in particular incurs a huge penalty. The first thing you lose is libraries—I'm guessing not many Ada packages are designed to avoid exceptions and the heap. Growable arrays and hash tables are right out.

Suppose you're willing to take that hit. It seems like there's also a cultural problem. For example, suppose your policy is that you need to prove all division operations won't cause divide-by-zero. This encourages programmers to change code like this:

  Velocity := Distance / DeltaT;

to this:

  if DeltaT = 0 then
    -- XXX very bad default value, will cause the missile to fall out
    -- of the sky; this can never happen though
    Velocity := 0;
  else
    Velocity := Distance / DeltaT;
  end if;

For some programmers, it'll always be easier to make this kind of change than to keep the code as-is and prove that DeltaT is never 0. Likewise, it's easier to delete an assertion than to prove it. (Maybe the solution is to have separate people responsible for code and proofs, but the web site doesn't mention this.)

I also saw nothing on the site about how robust the tools are against source code changes. Having to keep reproving things as the code undergoes minor changes sounds like a serious drag. Keeping unit tests up to date is hard enough.