Comment by zozbot234
18 hours ago
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.