3 ms·
"To me, in terms of the expectations of modern programming, the weird thing about proof languages is that they’re languages in the first place." I've got a sim
by mcguire 5y ago
"To me, in terms of the expectations of modern programming, the weird thing about proof languages is that they’re languages in the first place."
I've got a similar, but unrelated problem.
Most proof and formal methods languages development has involved dependently typed languages (modulo Frama-C and Spark). Which are dandy. However, the formula definitions are all in low-level, function-application-ish form, while the proof techniques are in high-level tactics. The result is that plain ol' simple formal logic is not directly applicable to using the formal techniques, and the proofs are completely unreadable.
Why aren't the formal techniques syntax-sugared into something understandable?
- throwaway17_17 5y agoI think the closest thing in usage is Liquid Haskell. Although not a standard proof, the ‘refinement’ types serve as a linearly solvable language of predicates on types. The syntax is relatively standard (in the way of set comprehensions), but it is limited to a subset of what can be captured with ‘full spectrum’ dependent types.
- junon 5y agoI'm in the exact same boat. I've been playing with a domain checker for a restricted set of C for a kernel project, specifically for this reason. But as of now I'm having to add better support for plugins in clang.