Re:Kind: A Modern Proof Language
by throwaway17_17 on Wednesday August 11, 2021 @04:01PM
(#28146999)
I 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.
I'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.
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?