Comment by zozbot234
18 hours ago
> When I wrote formal proofs, I used either TLA+ or Isabelle/HOL, neither of which are constructive.
True, but this requires using different formal systems for the algorithm and the proof. Isabelle/HOL being non-constructive means you can't fully express proof-carrying code in that single system, without tacking on something else for the "purely computational" added content.
That's not true. Non-constructive logics are extensions of constructive logics. You can express any algorithm in TLA+, and much more than algorithms.
You are right that when using non constructive logics, it's not guaranteed that the proof is executable as a program, but that's not a downside. Having the proof be a program in some sense is interesting, but it's not particularly useful.
How do you express computational content in non-constructive logic while both making it usable from proofs (e.g. if I have some algorithm that turns A's into B's, I want that to be directly referenceable in a proof - if A's have been posited, I must be able to turn them into B's) and keeping its character as specifically computational? Expressing algorithms in a totally separate way from proofs is arguably not much of a solution.
Not only is it easy, the ability to extend the computable into the non-computable is quite convenient. For example, computable numbers can be directly treated as a subset of the reals.
This is exactly how TLA+ works: https://pron.github.io/posts/tlaplus_part3
You create a subset or model of what's computable. Then, work in it. You might also prove refinements from high- to low-level forms.
Interestingly, we handle static analysis the same way by using language subsets. The larger chunk is unprovable. So, we just work with what's easy to analyze. Then, wrap it in types or contracts to use it properly.
And plenty of testing for when the specs are wrong.