The Coming Software Apocalypse

[nosystemdthanks]

as far as i know 6502 (and its nice to find you here again) the provability of programs was proven to be ultimately unprovable, no?

the halting problem, godels incompleteness theorems-- im just throwing out names, happy to leave this to people who are way better at math.

though whether the proof of unprovability defeats itself and merely shows that its impossible to prove that provability (even if you have your doubts...) yep, godel can take that one off our hands too... actually he cant, but we still cant prove it. and this is exactly why i struggled with math in school... probably.

[WIckedWitch]

as far as i know 6502 (and its nice to find you here again) the provability of programs was proven to be ultimately unprovable, no?

the halting problem, godels incompleteness theorems-- im just throwing out names, happy to leave this to people who are way better at math.

though whether the proof of unprovability defeats itself and merely shows that its impossible to prove that provability (even if you have your doubts...) yep, godel can take that one off our hands too... actually he cant, but we still cant prove it. and this is exactly why i struggled with math in school... probably.

Undecidability/unsolvability theorems generally do not undermine themselves because they work by examining the formal systems that they consider and, with suitably restricted principles of inference, show that the assumption of decidability/solvability leads to a contradiction. This is most easily seen in Turing's 1936 paper about the undecidability of the halting problem and that paper is relatively easy to follow, even by people who don't regard themselves as strong in mathematics.

Godel's proofs are harder but there is a gem of a booklet on them in the (sadly now defunct) Soviet/Russian series called, "The Little Mathematics Library". Getting beyond that into the later work of Tarski, things do get more demanding on the grey cells, so, unless you can't help yourslef, leave it at Turing and Godel.

Modern static analysis tools that try to produce correctness proofs for programs generally rely on restricted logical calculi that have tractable decision problems or on some form of bounded model checking.

SPARK Ada proof tools can now prove freedom from run-time error of 100k LOC in around two hours, AFAI recall. The top-end C static checkers also now use theorem provers but I don't have any verifiable performance data on them.

Th price of provability is that you must stick to a tractably verifiable subset of the programming language used. Obviously the SPARK prover requires restriction to the SPARK Ada language. For C programs you need to restrict to something stricter than MISRA C. Strengthening MISRA C by restricting it to a single-assignment programming style is probably the easiest approach here,

There are public-domain C static analysis tools developed by the Frama-C project in France if anyone is interested.