Purpose of proof: semi-formal methods

OK - I hereby declare a bias. I'm a PhD in mathematics, and I program soft-real-time semi-safety-critical systems.

Most people don't know what a proof in advance math is like. They seem to think it's all miniscule steps, starting from blindingly obvious miniscule statements, and build as a tedious, laborious, verging on infinitely long sequence of quantum-sized deductions.

It's not.

It's a way of imparting an understand of "what's really going on" and communicating that effectively.

Here's the proof that sqrt(2) is irrational as most people have seen it:

    suppose sqrt(2) = a/b
    then 2 = a^2/b^2
    hence 2 b^2 = a^2
    that means a^2 is even
    from that we know that a is even.

        we need to show that.
        suppose a is odd
        then a = 2k+1
        hence a^2 = (2k+1)^2
                  = 4k^2 + 4k + 1
        so if a is odd, a^2 is odd
        but a^2 is even
        hence a cannot be odd
        so a is even
        (end proof of mini-lemma)

    therefore we can write a=2k
    so 2 b^2 = (2k)^2
    so b^2 = 2k^2
    That means b^2 is even
    Using our mini-lemma, b is even
    so b = 2n
    Thus sqrt(2) = a/b = (2k)/(2n) = k/n
    But k and n are smaller than a and b.
    Repeating the above process gives an
        infinte descending sequence of
        positive whole numbers
    That's a contradiction.
    Therefore sqrt(2) cannot be a/b

    But the choice of a and b was arbitrary, 
    hence sqrt(2) is never a/b for any a or b

    Hence sqrt(2) is irrational.

That's what computer proofs of correctness are like.

Here's what a modern mathematician does:

    suppose sqrt(2) = a/b
    then 2 b^2 = a^2
    but the LHS has an odd number of factors of 2, 
    and the RHS has an even number of factors of 2.
    That can't work, so sqrt(2) is irrational.

Reasoning clearly, carefully and completely about code need not be the infinite suop of minutia people think it is, especially if you write the proof with the code. It's also important to write your code so that only small sections need truly detailed proofs. Error-robust code is a real winner.

The purpose of the code, the comments and the proof is to impart understanding to the reader. Yes, people will make mistakes in writing the proof, just as they make mistakes in writing the code, but having them both makes mistakes much less likely. Explaining both code and proof to colleagues reduces further the chances of error. Running tests to support the understanding does even more.

It will never be perfect, because the specification may have bugs, the compiler, the hardware, there may be cosmic rays that cause bit-flips. But having proofs, proper, human-style proofs, makes it much easier to have confidence.

In our experience it makes the code-production cycle faster and more predictable too, not to mention reducing the unpredictable bug-finding process.

Semi-formal proofs are a win all round, but in our experience most programmers can't do them. That's the problem we face.