3 ms·

Is there a good lecture series on Coq? Or maybe introductory project? I've seen a video intro [0] and poked a little bit around the reference manual [1], but I

Is there a good lecture series on Coq? Or maybe introductory project? I've seen a video intro [0] and poked a little bit around the reference manual [1], but I'm not sure what's "between" basic understanding of the commands and being able to extract a complex verified program. It all seems to be either the theory (which I mostly grok) or completed projects, not a lot about the engineering details. ...Or does that just not exist? [0] https://www.youtube.com/watch?v=ngM2N98ppQE https://www.youtube.com/watch?v=ngM2N98ppQE [1] https://coq.inria.fr/refman/ https://coq.inria.fr/refman/

TezlaOil 9y ago
Software Foundations book [1] covers many case studies. One of the authors has a lecture course based around the book as well. [1] softwarefoundations.cis.upenn.edu/current/index.html
- noch 9y ago
  Indeed: Benjamin Pierce's lectures on "Software Foundations in Coq" https://www.youtube.com/playlist?list=PLGCr8P_YncjUT7gXUVJWSoefQ40gTOz89 https://www.youtube.com/playlist?list=PLGCr8P_YncjUT7gXUVJWS...
- porges 9y ago
  I can recommend SF, I just started it a week ago without prior Coq experience. I'm using the VSCode integration which helps, CoqIDE is a bit clunky.
tanmitch 9y ago
In Coq to Rust Program Extraction https://news.ycombinator.com/item?id=12183095 https://news.ycombinator.com/item?id=12183095 , I saw some useful comments about its foundations. (And for a bit more about Coq to Rust, Program extraction from Coq https://github.com/rust-lang/rfcs/issues/667 https://github.com/rust-lang/rfcs/issues/667 )
nickpsecurity 9y ago
It's going to be hard to learn one way or another. Chlipala's Certified Programmimg with Dependent Types is free online. Then, Software Foundations others mentioned. Starting with lightweight stuff like Alloy or TLA+ might help. Also, The Little Prover book teaches how provers work by letting reader build a small one. Had some decent reviews.
- solomatov 9y ago
  Chlipala's book is a decent one, but it's oriented towards software verification, coq, and the use of tactics (which I would consider anti-pattern). Software Foundations is a good introduction to Coq and proofs, but overall is quite basic, and it also hides many details of how type theory works, so it's more of a hands on tutorial. TLA+ is just a tool which basically does its job by exhaustively searching a space of possible solutions trying to find counterexamples. It works in some limited cases but doesn't work generally for any mathematical theorem.
  - nickpsecurity 9y ago
    I bring up TLA+ because many people have quit trying to learn Coq because it was so hard with little perceived benefit. TLA+ has a high ratio of benefit for work put in. It also shows that abstract modeling can knock out deeper errors than regular tests or sometimes review. That makes it a nice, intermediate step toward stuff like Coq. Just a hunch a few of us have. :)
  - pron 9y ago
    > TLA+ is just a tool which basically does its job by exhaustively searching a space of possible solutions trying to find counterexamples. It works in some limited cases but doesn't work generally for any mathematical theorem. Nope. TLA+ is a rich mathematical formalism, that includes a full-fledged proof assistant. It is, however, focused on verifying software rather than arbitrary mathematical theorems. There is also a model checker for TLA+ that can check your theorems (about finite cases of programs) at the push of a button. In practice, model checkers works in more cases than manual proofs, as manual proofs "fail" much more often, simply by being far too laborious; a model checker would verify in days what may take you months or more to manually prove.
solomatov 9y ago
To really learn coq, you need to learn type theory which is hidden behind tactics. IMO, Coq isn't the best way to do so. I highly recommend starting with Agda instead.
- cmrx64 9y ago
  Lean hits a really good middle ground I think. More resources for Agda probably. But I'm very fond of lean ;)
  - solomatov 9y ago
    Lean is very interesting, but Agda and especially Coq has more learning resource, so for the beginners it's probably better to start from them, even though, in some sense Lean is more modern.
    - evincarofautumn 9y ago
      I have the impression that for someone coming from a programming background, Idris is also a pretty good introduction to the world of dependently typed programming and proof assistants.
solomatov 9y ago
Concerning the books on the topic, I highly recommend this: https://www.amazon.com/Verified-Functional-Programming-Agda-Books/dp/1970001240/ https://www.amazon.com/Verified-Functional-Programming-Agda-... If you want to get into the math related aspect, read this: https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/ There's also an annual summer school on the topic which has downloadable videos available: https://www.cs.uoregon.edu/research/summerschool/summer17/ https://www.cs.uoregon.edu/research/summerschool/summer17/
- Twisol 9y ago
  This year's OPLSS did not really engage with Coq. Adam Chlipala did give a lecture series on Coq at OPLSS'16 though: https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html https://www.cs.uoregon.edu/research/summerschool/summer15/cu... The DeepSpec summer school, however, did lead with a Coq intensive, which was recorded and included in the uploads at https://www.youtube.com/channel/UC5yB0ZRgc4A99ttkwer-dDw https://www.youtube.com/channel/UC5yB0ZRgc4A99ttkwer-dDw .
fpoling 9y ago
I have found Type-Driven Development with Idris [1] is a nice introduction into verifiable programming. The book starts with basic functional programming (Idris is how a strict Haskell could look) and gradually adds dependent types and working with proofs. [1] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...

TezlaOil 9y ago

Software Foundations book [1] covers many case studies. One of the authors has a lecture course based around the book as well. [1] softwarefoundations.cis.upenn.edu/current/index.html

noch 9y ago
Indeed: Benjamin Pierce's lectures on "Software Foundations in Coq" https://www.youtube.com/playlist?list=PLGCr8P_YncjUT7gXUVJWSoefQ40gTOz89 https://www.youtube.com/playlist?list=PLGCr8P_YncjUT7gXUVJWS...
porges 9y ago
I can recommend SF, I just started it a week ago without prior Coq experience. I'm using the VSCode integration which helps, CoqIDE is a bit clunky.

tanmitch 9y ago

In Coq to Rust Program Extraction https://news.ycombinator.com/item?id=12183095 https://news.ycombinator.com/item?id=12183095 , I saw some useful comments about its foundations. (And for a bit more about Coq to Rust, Program extraction from Coq https://github.com/rust-lang/rfcs/issues/667 https://github.com/rust-lang/rfcs/issues/667 )

nickpsecurity 9y ago

It's going to be hard to learn one way or another. Chlipala's Certified Programmimg with Dependent Types is free online. Then, Software Foundations others mentioned. Starting with lightweight stuff like Alloy or TLA+ might help. Also, The Little Prover book teaches how provers work by letting reader build a small one. Had some decent reviews.

solomatov 9y ago
Chlipala's book is a decent one, but it's oriented towards software verification, coq, and the use of tactics (which I would consider anti-pattern). Software Foundations is a good introduction to Coq and proofs, but overall is quite basic, and it also hides many details of how type theory works, so it's more of a hands on tutorial. TLA+ is just a tool which basically does its job by exhaustively searching a space of possible solutions trying to find counterexamples. It works in some limited cases but doesn't work generally for any mathematical theorem.
- nickpsecurity 9y ago
  I bring up TLA+ because many people have quit trying to learn Coq because it was so hard with little perceived benefit. TLA+ has a high ratio of benefit for work put in. It also shows that abstract modeling can knock out deeper errors than regular tests or sometimes review. That makes it a nice, intermediate step toward stuff like Coq. Just a hunch a few of us have. :)
- pron 9y ago
  > TLA+ is just a tool which basically does its job by exhaustively searching a space of possible solutions trying to find counterexamples. It works in some limited cases but doesn't work generally for any mathematical theorem. Nope. TLA+ is a rich mathematical formalism, that includes a full-fledged proof assistant. It is, however, focused on verifying software rather than arbitrary mathematical theorems. There is also a model checker for TLA+ that can check your theorems (about finite cases of programs) at the push of a button. In practice, model checkers works in more cases than manual proofs, as manual proofs "fail" much more often, simply by being far too laborious; a model checker would verify in days what may take you months or more to manually prove.

solomatov 9y ago

To really learn coq, you need to learn type theory which is hidden behind tactics. IMO, Coq isn't the best way to do so. I highly recommend starting with Agda instead.

cmrx64 9y ago
Lean hits a really good middle ground I think. More resources for Agda probably. But I'm very fond of lean ;)
- solomatov 9y ago
  Lean is very interesting, but Agda and especially Coq has more learning resource, so for the beginners it's probably better to start from them, even though, in some sense Lean is more modern.
  - evincarofautumn 9y ago
    I have the impression that for someone coming from a programming background, Idris is also a pretty good introduction to the world of dependently typed programming and proof assistants.

solomatov 9y ago

Concerning the books on the topic, I highly recommend this: https://www.amazon.com/Verified-Functional-Programming-Agda-Books/dp/1970001240/ https://www.amazon.com/Verified-Functional-Programming-Agda-... If you want to get into the math related aspect, read this: https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/ There's also an annual summer school on the topic which has downloadable videos available: https://www.cs.uoregon.edu/research/summerschool/summer17/ https://www.cs.uoregon.edu/research/summerschool/summer17/

Twisol 9y ago
This year's OPLSS did not really engage with Coq. Adam Chlipala did give a lecture series on Coq at OPLSS'16 though: https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html https://www.cs.uoregon.edu/research/summerschool/summer15/cu... The DeepSpec summer school, however, did lead with a Coq intensive, which was recorded and included in the uploads at https://www.youtube.com/channel/UC5yB0ZRgc4A99ttkwer-dDw https://www.youtube.com/channel/UC5yB0ZRgc4A99ttkwer-dDw .

fpoling 9y ago

I have found Type-Driven Development with Idris [1] is a nice introduction into verifiable programming. The book starts with basic functional programming (Idris is how a strict Haskell could look) and gradually adds dependent types and working with proofs. [1] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...