a thoughtful web.
Good ideas and conversation. No ads, no tracking.   Login or Take a Tour!
comment by kingmudsy
kingmudsy  ·  1099 days ago  ·  link  ·    ·  parent  ·  post: Proving the relationship between the golden ratio and the Fibonnaci numbers in Coq

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!

ilex  ·  1098 days ago  ·  link  ·  

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.

Also I like roosters

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 :)