What the page presents is a tool for producing mathematical proofs. Proofs are really useful for mathematicians for with them you can derive lots of truths abou

What the page presents is a tool for producing mathematical proofs. Proofs are really useful for mathematicians for with them you can derive lots of truths about mathematical objects. For example, it is true that if q^2 = 2, then q is not a rational number. In the same way, using the tool on the page you can prove that 1. the while-loop terminates. 2. the invariants hold, meaning that your program is correct. Yes, you can encode the proof in a machine-checkable format but that is missing some of the point. Just like with mathematical proofs, the major use of the proof is to communicate with humans. Also the same techniques used to prove invariants by hand can be used by compilers to implement smart optimizations. In the sum example, the compiler could deduce/prove that sum = \sum_{i=1}^n i and replace the loop body with n(n+1)/2. I don't know if any compilers do such advanced optimizations but theoretically they could (in trivial cases like these - in general, proving properties about code is as hard as solving the halting problem). Other proof techniques involve finding upper and lower limits of variables which are used to store values in more efficient types. For example, storing an integer as an int32 instead of int64. To really understand what's going on read https://en.wikipedia.org/wiki/Hoare_logic https://en.wikipedia.org/wiki/Hoare_logic. The article's proof uses Hoare logic but implicitly, without the notation, so understanding how the proofs work is hard.