3 ms·
There is an interactive tutorial at [1]. I find this quite amazing. With refinement types one can say/prove things like: - This function only returns even num
by airesQ 10y ago
There is an interactive tutorial at [1].
I find this quite amazing. With refinement types one can say/prove things like:
- This function only returns even numbers.
- The input for this function is not just any vector, it must be an ordered vector.
- It's possible to make compile time unit tests. Where we write a function that exercises the code, and returns True if the test succeeds. Then one adds a refinement type saying that the function must always evaluate to true. The theorem prover does the rest.
[1] - http://ucsd-progsys.github.io/liquidhaskell-tutorial/02-logic.html#/examples-arithmetic http://ucsd-progsys.github.io/liquidhaskell-tutorial/02-logi...
- jeff_marshall 10y agoThere have been quite a few systems that can handle proofs of the kinds of propositions you list above using various different logical frameworks, programming languages, and automatic and/or user-guided proof assistants. That said, it's no small feat to do a correct translation from the semantics of a full, modern, programming language into the semantics of a SMT solver (which appears to be the primary back-end for deciding propositions in this tool). I'll have to go read the actual dissertation to see how far that goes and whether any escape-hatches for user guidance exist (tactics, manual term manipulation, etc.). I haven't yet found a tool that doesn't allow extensive user guidance to be all that effective for proving things about code/systems that are interesting (to me).