A proof is much harder in the OOP world because of side effects, unrestricted inheritance, and null being a member of every type. Most proofs rely on an induction principle to show that you’ve covered every possibility, and all 3 of those things make that harder to prove.

Let’s say we’re implementing binary trees that contain integer values (for the sake of keeping the syntax simpler, I won’t bring generic programming into this, though it wouldn’t change anything.) In Standard ML, I would define that like this:

datatype tree = Empty | Node of (tree * int * tree)

This introduces a new type called tree whose values can come in exactly two varieties (or classes, not to be confused with the OOP concept of a class) – an Empty value which carries no information, and Node values which carry a 3-tuple whose first and last elements are trees and whose middle element is an int. The closest approximation to this declaration in OOP would look like this:

public class Tree {
    private Tree() {} // Prevent external subclassing

    public static final class Empty extends Tree {}

    public static final class Node extends Tree {
        public final Tree leftChild;
        public final int value;
        public final Tree rightChild;

        public Node(Tree leftChild, int value, Tree rightChild) {
            this.leftChild = leftChild;
            this.value = value;
            this.rightChild = rightChild;
        }
    }
}

With the caveat that variables of type Tree can never be null.

Now let’s write a function to calculate the height (or depth) of the tree, and assume we have access to a max function that returns the larger of two numbers:

fun height(Empty) =
        0
 |  height(Node (leftChild, value, rightChild)) =
        1 + max( height(leftChild), height(rightChild) )

We’ve defined the height function by cases – there’s one definition for Empty trees and one definition for Node trees. The compiler knows how many classes of trees exist and would issue a warning if you didn’t define both cases. The expression Node (leftChild, value, rightChild) in the function signature binds the values of the 3-tuple to the variables leftChild, value, and rightChild respectively so we can refer to them in the function definition. It’s akin to having declared local variables like this in an OOP language:

Tree leftChild = tuple.getFirst();
int value = tuple.getSecond();
Tree rightChild = tuple.getThird();

How can we prove we’ve implemented height correctly? We can use structural induction, which consists of:
1. Prove that height is correct in the base case(s) of our tree type (Empty)
2. Assuming that recursive calls to height are correct, prove that height is correct for the non-base case(s) (when the tree is actually a Node).

For step 1, we can see that the function always returns 0 when the argument is an Empty tree. This is correct by definition of the height of a tree.

For step 2, the function returns 1 + max( height(leftChild), height(rightChild) ). Assuming that the recursive calls truly do return the height of the children, we can see that this is also correct.

And that completes the proof. Steps 1 and 2 combined exhaust all the possibilities. Note, however, that we have no mutation, no nulls, and there are exactly two varieties of trees. Take away those three conditions and the proof quickly becomes more complicated, if not impractical.

EDIT: Since this answer has risen to the top, I’d like to add a less trivial example of a proof and cover structural induction a bit more thoroughly. Above we proved that if height returns, its return value is correct. We haven’t proved it always returns a value, though. We can use structural induction to prove this, too (or any other property.) Again, during step 2, we’re allowed to assume the property holds of the recursive calls as long as the recursive calls all operate on a direct child of the tree.

A function can fail to return a value in two situations: if it throws an exception, and if it loops forever. First let’s prove that if no exceptions are thrown, the function terminates:

1. Prove that (if no exceptions are thrown) the function terminates for the base cases (Empty). Since we unconditionally return 0, it terminates.

2. Prove that the function terminates in the non-base cases (Node). There’s three function calls here: +, max, and height. We know that + and max terminate because they’re part of the language’s standard library and they’re defined that way. As mentioned earlier, we’re allowed to assume the property we’re trying to prove is true on recursive calls as long as they operate on immediate subtrees, so calls to height terminate too.

That concludes the proof. Note that you wouldn’t be able to prove termination with a unit test. Now all that’s left is to show that height doesn’t throw exceptions.

1. Prove that height doesn’t throw exceptions on the base case (Empty). Returning 0 can’t throw an exception, so we’re done.
2. Prove that height doesn’t throw exception on the non-base case (Node). Assume once again that we know + and max don’t throw exceptions. And structural induction allows us to assume the recursive calls won’t throw either (because the operate on the tree’s immediate children.) But wait! This function is recursive, but not tail recursive. We could blow the stack! Our attempted proof has uncovered a bug. We can fix it by changing height to be tail recursive.

I hope this shows proofs don’t have to be scary or complicated. In fact, whenever you write code, you’ve informally constructed a proof in your head (otherwise, you wouldn’t be convinced you just implemented the function.) By avoiding null, unnecessary mutation, and unrestricted inheritance you can prove your intuition is correct fairly easily. These restrictions are not as harsh as you might think:

• null is a language flaw and doing away with it is unconditionally good.
• Mutation is sometimes unavoidable and necessary, but it’s needed a lot less often than you’d think – especially when you have persistent data structures.
• As for having a finite number of classes (in the functional sense)/subclasses (in the OOP sense) vs an unlimited number of them, that’s a subject too big for a single answer. Suffice to say there’s a design trade off there – provability of correctness vs flexibility of extension.

1. It is a lot easier to reason about code when everything is immutable. As a result, loops are more often written as recursion. In general, it’s easier to verify correctness of a recursive solution. Often, such a solution will also read very similarly to a mathematical definition of the problem.

   However, there is very little motivation to carry out an actual formal proof of correctness in most cases. Proofs are difficult, take a lot (human) time, and have a low ROI.

2. Some functional languages (esp. from the ML family) have extremely expressive type systems that can make much more complete guarantees that a C-style type system (but some ideas like generics have become common in mainstream languages as well). When a program passes a type check, this is a kind of automated proof. In some cases, this will be able to detect some errors (e.g. forgetting the base case in a recursion, or forgetting to handle certain cases in a pattern match).

   On the other hand, these type systems have to be kept very limited in order to keep them decidable. So in a sense, we gain static guarantees by giving up flexibility – and these restrictions are a reason why complicated academic papers along the lines of “A monadic solution to a solved problem, in Haskell” exist.

   I enjoy both very liberal languages, and very restricted languages, and both have their respective difficulties. But it’s not the case that one would be “better”, each is just more convenient for a different kind of task.

Then it has to be pointed out that proofs and unit testing are not interchangeable. They both allow us to put bounds on the correctness of the program:

• Testing puts an upper bound on correctness: If a test fails, the program is incorrect, if no tests fail, we are certain that the program will handle the tested cases, but there may still be undiscovered bugs.

  int factorial(int n) {
    if (n <= 1) return 1;
    if (n == 2) return 2;
    if (n == 3) return 6;
    return -1;
  }
  
  assert(factorial(0) == 1);
  assert(factorial(1) == 1);
  assert(factorial(3) == 6);
  // oops, we forgot to test that it handles n > 3…
  

• Proofs put a lower bound on correctness: It may be impossible to prove certain properties. For example, it may be easy to prove that a function always returns a number (that’s what type systems do). But it may be impossible to prove that the number will always be < 10.

  int factorial(int n) {
    return n;  // FIXME this is just a placeholder to make it compile
  }
  
  // type system says this will be OK…
  

A word of warning may be in order here:

While it is generally true what others write here – in short, that advanced type systems, immutablity and referential transparency contribute a lot to correctness – it is not the case that testing is not done in the functional world. To the contrary!

This is because we have tools like Quickcheck, that generate test cases automatically and randomly. You merely state the laws that a function must obey, and then quickcheck will check these laws for hundreds of random test cases.

You see, this is a bit higher level than trivial equality checks on a handful of test cases.

Here is an example from an implementation of an AVL tree:

--- A generator for arbitrary Trees with integer keys and string values
aTree = arbitrary :: Gen (Tree Int String)


--- After insertion, a lookup with the same key yields the inserted value        
p_insert = forAll aTree (t -> 
             forAll arbitrary (k ->
               forAll arbitrary (v ->
                lookup (insert t k v) k == Just v)))

--- After deletion of a key, lookup results in Nothing
p_delete = forAll aTree (t ->
            not (null t) ==> forAll (elements (keys t)) (k ->
                lookup (delete t k) k == Nothing))

The second law (or property) we can read as follows: For all arbitrary trees t, the following holds: if t is not empty, then for all the keys k of that tree it will hold that looking up k in the tree that is the result of deleting k from t, the result will be Nothing (which indicates: not found).

This checks proper functionality for deletion of an existing key. What laws should govern the deletion of a non-existing key? We certainly want the resulting tree to be the same as the one we deleted from. We can express this easily:

p_delete_nonexistant = forAll aTree (t ->
                          forAll arbitrary (k -> 
                              k `notElem` keys t ==> delete t k == t))

This way, testing is really fun. And besides, once you learn to read quickcheck properties, they serve as a machine testable specification.

I don’t exactly understand what the linked answer means by “achieve modularity through mathematical laws”, but I think I have an idea of what is meant.

Check out Functor:

The Functor class is defined like this:

 class Functor f where
   fmap :: (a -> b) -> f a -> f b

It doesn’t come with test cases, but rather, with a couple of laws that must be satisfied.

All instances of Functor should obey:

 fmap id = id
 fmap (p . q) = (fmap p) . (fmap q)

Now let’s say you implement Functor (source):

instance  Functor Maybe  where
    fmap _ Nothing       = Nothing
    fmap f (Just a)      = Just (f a)

The problem is to verify that your implementation satisfies the laws. How do you go about doing that?

One approach is to write test cases. The fundamental limitation of this approach is that you’re verifying the behavior in a finite number of cases (good luck exhaustively testing a function with 8 parameters!), and so passing tests can’t guarantee anything but that the tests pass.

Another approach is to use mathematical reasoning, i.e. a proof, based on the actual definition (instead of on the behavior in a limited number of cases). The idea here is that a mathematical proof may be more effective; however, this depends on how amenable your program is to mathematical proof.

I can’t guide you through an actual formal proof that the above Functor instance satisfies the laws, but I’ll try and give an outline of what the proof might look like:

1. fmap id = id
   • if we have Nothing
     • fmap id Nothing = Nothing by part 1 of the implementation
     • id Nothing = Nothing by the definition of id
   • if we have Just x
     • fmap id (Just x) = Just (id x) = Just x by part 2 of the implementation, then by the definition of id
2. fmap (p . q) = (fmap p) . (fmap q)
   • if we have Nothing
     • fmap (p . q) Nothing = Nothing by part 1
     • (fmap p) . (fmap q) $ Nothing = (fmap p) $ Nothing = Nothing by two applications of part 1
   • if we have Just x
     • fmap (p . q) (Just x) = Just ((p . q) x) = Just (p (q x)) by part 2, then by the definition of .
     • (fmap p) . (fmap q) $ (Just x) = (fmap p) $ (Just (q x)) = Just (p (q x)) by two applications of part two

“Beware of bugs in the above code; I have only proved it correct, not tried it.”
– Donald Knuth

In a perfect world, programmers are perfect and don’t do mistakes, so there are no bugs.

In a perfect world, computer scientists and mathematicians are also perfect, and don’t do mistakes either.

But we don’t live in a perfect world. So we can’t rely on programmers to make no mistakes. But we can’t assume that any computer scientist who delivers a mathematical proof that a program is correct didn’t make any mistakes in that proof. So I wouldn’t pay any attention to anyone trying to proof that his code works. Write unit-tests and show me that the code behaves according to specifications. Anything else won’t convince me of anything.