Home

Verified Programming in Guru

Verified Programming in Guru is a tutorial introduction to Guru:

GURU is a pure functional programming language, which is similar in some ways to Caml and Haskell. But GURU also contains a language for writing formal proofs demonstrating the properties of programs. So there are really two languages: the language of programs, and the language of proofs.

In comparison to Coq:

GURU is inspired largely by the COQ theorem prover, used for formalized mathematics and theoretical computer science, as well as program verification. Like COQ, GURU has syntax for both proofs and programs, and supports dependent types. GURU does not have as complex forms of polymorphism and dependent types as COQ does. But GURU supports some features that are difficult or impossible for COQ to support, which are useful for practical program verification. In COQ, the compiler must be able to confirm that all programs are uniformly terminating: they must terminate on all possible inputs. We know from basic recursion theory or theoretical computer science that this means there are some programs which really do terminate on all inputs that the compiler will not be able to confirm do so. Furthermore, some programs, like web servers or operating systems, are not intended to terminate. So that is a significant limitation. Other features GURU has that COQ lacks include support for functional modeling of non-functional constructs like destructive updates of data structures and arrays; and better support for proving properties of dependently typed functions.

The tutorial is worth a read to anybody new to this style of programming as it is one of the most gentle introductions to dependent types and automated program verification that I've seen.

By James Iry at 2009-08-05 02:59 | Logic/Declarative | Meta-Programming | Teaching & Learning | Type Theory | other blogs | 13462 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Excellent

We need more tools like this one to get to mainstream programming. Bravo.

By andrejbauer at Wed, 2009-08-05 07:17 | login or register to post comments

Nice

This looks good indeed as a gentle introduction to the material, but it's worth pointing out that the author seems a bit confused in some respects: Coq is a theorem prover and programming environment based on Type Theory and the Curry-de Bruijn-Howard Isomorphism, so it can't support general recursion any more than any other such pairing can, because by the isomorphism, divergence == unsoundness (that is, divergence is isomorphic to "falsum" or "bottom," from which you can prove anything). But the point that you want to be able to say meaningful things about non-terminating processes like servers is a good one, so Coq supports coinduction and corecursion, and much recent work has been done to generalize their application. See in particular Inductive and Coinductive Components of Corecursive Functions in Coq and its slides (PDF). Imperative programming in Coq is, of course, part of the subject matter of the YNot project.

Eh. With all of that said, I have no doubt that many people will be served by this effort, which seems more closely related to other languages closer to the "programming language" end of the spectrum vs. "theorem prover" end, such as Epigram and Agda, than to Coq. But especially with YNot, I wonder if Coq isn't beginning to catch up... see the stories I'm about to write for the front page. :-)

By Paul Snively at Thu, 2009-08-06 16:14 | login or register to post comments

the more the merrier

can't help but be excited to see ever more development along these lines. who knows, maybe some day mainstream software will suck just a little bit less.

By raould at Thu, 2009-08-06 19:13 | login or register to post comments