Mathematically Structured but not Necessarily Functional Programming
- 29 May 2009
- Computation, Constructive math, Programming, RZ, Talks
These are the slides and the extended abstract from my MSFP 2008 talk. Apparently, I forgot to publish them online. There is a discussion on the Agda mailing list to which the talk is somewhat relevant, so I am publishing now.
Abstract: Realizability is an interpretation of intuitionistic logic which subsumes the Curry-Howard interpretation of propositions as types, because it allows the realizers to use computational effects such as non-termination, store and exceptions. Therefore, we can use realizability as a framework for program development and extraction which allows any style of programming, not just the purely functional one that is supported by the Curry-Howard correspondence. In joint work with Christopher A. Stone we developed RZ, a tool which uses realizability to translate specifications written in constructive logic into interface code annotated with logical assertions. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools. In our experience, RZ is useful for specification of non-trivial theories. While the use of computational effects does improve efficiency it also makes it difficult to reason about programs and prove their correctness. We demonstrate this fact by considering non-purely functional realizers for a Brouwerian continuity principle.
Download: msfp2008-slides.pdf, msfp2008-abstract.pdf
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
Comments
The Ynot project is worth looking at: http://ynot.cs.harvard.edu. Although in theory whatever you could write in Ocaml you could write in Coq+Ynot, in practice it is probably not so easy. RZ has an advantage for the programmer who does not need to provide a formal proof of correctness.
As for the connection between effects and constructive reasoning, there is a point which I think is often overlooked by constructivists, that at least for some effects there is a corresponding Curry-Howard-isomorphic logic : classical logic. An example is the lambda-mu-calculus of Parigot. One problem with computational classical logic, however, is that it is not clear how to take it to dependent types.
[...] See the rest here: Mathematics and Computation » Mathematically Structured but not … [...]