__Login__or

__Take a Tour__!

This is really, *really* cool from a conceptual perspective. At the same time, I'm immensely glad that I don't have to work with this professionally :)

Do you have an end-goal in mind for learning Coq, or is it more of a curiosity you want to satisfy? Curious to see what else you might try with the language!

I also find this *way cool*. You will probably enjoy Wadler's *Propositions as Types* if you want to understand the proof/program thing in more detail.

I am generally interested in program analysis and theorem proving and that sort of thing. I picked it up to maybe use it with my research, since being able to generate proofs and extract executable code is pretty handy, but we'll see if I can become competent in it fast enough to be able to actually apply it.

I did write another thing about using Coq that shows some of the proof state as you go. The interactive part really makes writing proofs possible; I don't know if I could just look at something and write all the ltac for it without any help. This is a bit more along the lines of what I'm doing for research, but still a long ways from what counts as cutting-edge nowadays :)