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.
Recent comments
2 days 4 hours ago
3 days 23 hours ago
2 weeks 1 day ago
3 weeks 4 hours ago
4 weeks 2 hours ago
5 weeks 5 days ago
6 weeks 1 day ago
7 weeks 1 day ago
7 weeks 5 days ago
7 weeks 5 days ago