I've been looking for an excuse to play with Coq (cough) for awhile now. A new release is as good an excuse as any I suppose.
Does anyone know how this compares to something like Idris?
Does anyone know how this compares to something like Idris?
- Gallina, which is a pure functional programming language a lot like Idris, which is used in 'straightforward' definitions.
- Ltac, which is an awkward imperative language for incrementally building up proof objects using a variety of "tactic" primitives. Ltac is executed at compile time to generate values which would be cumbersome or impossible to write directly in Gallina (a bit like Lisp macros).
Most of Coq's power is exposed via Ltac, e.g. most of the proofs in http://adam.chlipala.net/cpdt/ are generalised into powerful Ltac functions; the reason for this is explained at http://adam.chlipala.net/cpdt/html/Cpdt.Large.html
Unfortunately, this focus on Ltac has left Gallina a little impoverished. For example, dependent matching in Gallina is pretty horrible (compared to, say, Agda; although there are complications there e.g. with the K axiom), whereas in Ltac we can simply use a tactic like `destruct`.
Personally, I'm a fan of http://plv.mpi-sws.org/mtac/ which allows regular Gallina, along with a few extensions, to be used instead of Ltac. Basically, any 'unsafe' action which we might have done in Ltac, like general recursion, gets wrapped up in a monadic datatype "M". During compilation, "M foo" values can be forced to get the "foo" value they wrap, which are inserted into the output just like Ltac results. If that forcing fails, or loops forever, so does the compilation (again, like Ltac).
Mtac feels a lot like using Idris IMHO.
It would be closer to "caught" \kɔːt\ with a short vowel and a \k\ sound at the end.
EDIT: I may have a slight bias as a "General American" user, but I just noticed the parent actually also includes a length suprasegmental modifier, which probably means they're a Received Pronunciation English speaker, or copy-pasted the IPA from somewhere :-D. At any rate, my point that "it sounds like the vowel in 'caught' is pretty ambiguous" still stands.