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

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