4 ms·

I just finished a course in Coq - it was pretty fun. Seems like something of the same the guys paper is about.

ekarulf 12y ago
My discrete math and logic undergraduate course was in Coq. It was a brutal way to learn the proof process at first but it was worth the investment by the end. It's the logic equivalent of TDD. If you are interested in computational logic you might enjoy Aaron Stump from UIowa's work: https://queuea9.wordpress.com/ https://queuea9.wordpress.com/
ipsum2 12y ago
The article has nothing to do with Coq: > When I saw the title of the talk, I assumed Lamport would be talking about computer proof checking programs or even a proof creating program like the one Timothy Gowers has worked on and written about. But Lamport’s advice was much more down-to-earth.
- madsravn 12y ago
  I'm a referring the guys paper, which is linked here in the comments somewhere. There TLA+ is mentioned which is a tool to formally prove something. The same can be done in Coq - which is why I'm drawing a parallel.
  - tel 12y ago
    While that parallel is genuine, it's hard to compare Coq and TLA+ since the mechanism and style of proof they embody is very different. TLA+ tries to ensure that you can exhaustively check implied models as its basis of proof (I believe) while Coq recognizes that types syntactically represent logics and we can thus construct programs in those logics to represent proofs. So, one layer deeper they're dramatically different beasts.
    - swatow 12y ago
      you are correct. There is a huge difference between the two and as you say only coq is able to express proofs in themselves and not just a coarse grained summary of their structure.
    - grogers 12y ago
      The TLA+ tools can do exhaustive model checking, as well as mechanically checked proofs. The proofs typically use an SMT solver to verify them. Of the two I've only used model checking in a serious way, but you can find Lamport's proofs of things like paxos and have it turn all the theorems green.
      - tel 12y ago
        SMT is still a pretty far cry from type theoretic proof. At the end of the day it's just another kind of exhaustiveness checker.

My discrete math and logic undergraduate course was in Coq. It was a brutal way to learn the proof process at first but it was worth the investment by the end. It's the logic equivalent of TDD. If you are interested in computational logic you might enjoy Aaron Stump from UIowa's work: https://queuea9.wordpress.com/ https://queuea9.wordpress.com/

ipsum2 12y ago

The article has nothing to do with Coq: > When I saw the title of the talk, I assumed Lamport would be talking about computer proof checking programs or even a proof creating program like the one Timothy Gowers has worked on and written about. But Lamport’s advice was much more down-to-earth.

madsravn 12y ago
I'm a referring the guys paper, which is linked here in the comments somewhere. There TLA+ is mentioned which is a tool to formally prove something. The same can be done in Coq - which is why I'm drawing a parallel.
- tel 12y ago
  While that parallel is genuine, it's hard to compare Coq and TLA+ since the mechanism and style of proof they embody is very different. TLA+ tries to ensure that you can exhaustively check implied models as its basis of proof (I believe) while Coq recognizes that types syntactically represent logics and we can thus construct programs in those logics to represent proofs. So, one layer deeper they're dramatically different beasts.
  - swatow 12y ago
    you are correct. There is a huge difference between the two and as you say only coq is able to express proofs in themselves and not just a coarse grained summary of their structure.
  - grogers 12y ago
    The TLA+ tools can do exhaustive model checking, as well as mechanically checked proofs. The proofs typically use an SMT solver to verify them. Of the two I've only used model checking in a serious way, but you can find Lamport's proofs of things like paxos and have it turn all the theorems green.
    - tel 12y ago
      SMT is still a pretty far cry from type theoretic proof. At the end of the day it's just another kind of exhaustiveness checker.