Formal verification?

Formal verification of software is quite a dialectic activity. From the absolute mathematical perspective it is theoretically impossible, from an industrial perspective it is more than feasible. How do we live with that? Actually there exist very simple programs, whose verification is equivalent to solving unsolved or very complicated mathematical theorems. Imagine the pseudocode like that:

function cantor_advance (uint x, uint y, uint z, uint n)
{
…
}

function fermat_test () {
uint x, y, z = 1;
uint n = 3;

while true do {

  // check Fermat’s theorem equality
  if (x^n + y^n == z^n) break;

  // uniformly increment quadruple using
  // 4D analogue of the Cantor diagonalization method

  (x,y,z,n) = cantor_advance(x,y,z,n);
}

print (x,y,z,n);

}        

It is obvious that proving the termination of such an internal loop will be equivalent to refutation of the Fermat’s Last theorem which is known to be proven in a way lying much further than an ordinary erudition. So the loop actually never terminates (modulo hardware restrictions).

Many experts fairly think that the root of formal methods failures lies in loops, especially when they are performed over infinite collections (like while true). But actually not only. The second root is … natural arithmetic. Just adding the standard arithmetic operations makes the loops unpredictable in terms of termination. If we leave only types with finite cardinality, like booleans, and bounded collections of them, even for possibly infinite loops, the number of variants is also finite and can be at least brute forced. A loop can still be interminable but it will contain state cycles within and that fact can be proven. The actual explanation can be expressed in terms of G?del incompleteness and Tarski undefinability theorems and its correspondence to the Turing machine halting problem.

So why do we still think that formal methods are great in CS and provide an unprecedented way of software security and correctness? Very simple: there is too little reason to write a program with full uncertainty of its termination - and the internal explanation of why a program terminates can be just true or false. This explanation rarely involves deep mathematical theories and that is why can be deductively proven. However humanity is still on its path to make the software verification more affordable for businesses.