The Prover company is working on the safety of train signalling software. Basically, they seek to prove that a given program is “safe” along a number of formal criteria. It involves the translation of the program in some (boolean based) standard form, which is then analysed.
The formal criteria are chosen manually, but the proofs are found completely automatically.
Despite the sizeable length of the proofs, combinatorial explosion is generally avoided, because programs written by humans (and therefore their standard form translation) tend to have shapes that lend them amenable to massive cuts in the search tree.
It doesn’t always work: first, the criteria are simple and bounded. Second, combinatorial explosion sometimes does occur, in which case human-devised tweaks are needed.
Oh, and it’s all proprietary. Maybe there’s some related academic papers, though.
The key part is that some of those formal verification processes involve automated proof generation. This is exactly what Jonah is talking about:
I don’t know of any computer programs that have been able to prove theorems outside of the class “very routine and not requiring any ideas,” without human assistance (and without being heavily specialized to an individual theorem).
Those who make (semi-)automated proof for a living have a vested interest in making such things as useful as possible. Among other things, this means as automated as possible, and as general as possible. They’re not there yet, but they’re definitely working on it.
The Prover company is working on the safety of train signalling software. Basically, they seek to prove that a given program is “safe” along a number of formal criteria. It involves the translation of the program in some (boolean based) standard form, which is then analysed.
The formal criteria are chosen manually, but the proofs are found completely automatically.
Despite the sizeable length of the proofs, combinatorial explosion is generally avoided, because programs written by humans (and therefore their standard form translation) tend to have shapes that lend them amenable to massive cuts in the search tree.
It doesn’t always work: first, the criteria are simple and bounded. Second, combinatorial explosion sometimes does occur, in which case human-devised tweaks are needed.
Oh, and it’s all proprietary. Maybe there’s some related academic papers, though.
I don’t think this is what Jonah is talking about. This is just one of thousands of examples of formal verification of safety-critical software.
The key part is that some of those formal verification processes involve automated proof generation. This is exactly what Jonah is talking about:
Those who make (semi-)automated proof for a living have a vested interest in making such things as useful as possible. Among other things, this means as automated as possible, and as general as possible. They’re not there yet, but they’re definitely working on it.