10 ms·

Software Foundations by Benjamin Pierce et al.

95 points by nextos 11y ago

Pils 11y ago
Working through this right now as a directed reading with a professor and a couple of other students. Would definitely recommend this as a follow up to an intro PL course.
bkase 11y ago
Certified Programming with Dependent Types (available online as well http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/) is also a good resource for learning Coq (note: I just started working through the material this weekend).
javajosh 11y ago
Uh, how do you pronounce Coq?
- cmrx64 11y ago
  https://translate.google.com/#fr/en/coq https://translate.google.com/#fr/en/coq, click "listen". Or, in French IPA (https://en.wikipedia.org/wiki/Help:IPA_for_French https://en.wikipedia.org/wiki/Help:IPA_for_French), kɔk (roughly transcribed to English, "couk") But, everyone I know (including me) who I've heard pronunce it just pronunces it "cock".
- tel 11y ago
  As is traditional: You pronounce it with an understanding of how difficult it must be to speak French and have most of the CS world talk about bit twiddling.
  - pron 11y ago
    :)
davidgrenier 11y ago
Whatever your views on that stuff... it is fun to play in Coq. On the other hand, playing with J-Bob, the toy "proof assistant" used in The Little Prover is tedious at best. I'm torn between just giving up with the last two chapters of the book undone.
cmrx64 11y ago
This is a lovely book. I gathered a group of students to work through this book last year (and even roped in a professor). If you're interested in formal software verification or interactive proof assistants, this is an excellent and approachable introduction. Another free book, using the Isabelle proof assistant, is http://concrete-semantics.org/ http://concrete-semantics.org/. It's also very good.
- nextos 11y ago
  It looks very nice. The Little Prover, recently published is also a neat small intro. I wonder how does Software Foundations compare against other more specialized classics in the field like [1-3]. [1] https://mitpress.mit.edu/books/principles-model-checking https://mitpress.mit.edu/books/principles-model-checking [2] http://www.springer.com/fr/book/9783540654100 http://www.springer.com/fr/book/9783540654100 [3] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/
  - cmrx64 11y ago
    I've worked through TaPL too. I'm not even sure they are comparable :) It's possible to formalize the contents of TaPL in these systems (and, indeed, Pierce has taught it like that). But it's still a very different focus than Software Foundations. I've not read or worked through the other books (wow they are expensive), but I'm in general not very keen on model checking as an approach. Tools like Alloy or NuSMV can be useful when designing or investigating algorithms, but they always do a bounded search and can't be applied directly to implementations. I personally don't confer that much trustworthyness to systems that appeal to model checking tools for their correctness. I've seen The Little Prover, but am somewhat wary of it. On the other hand, I enjoyed The Little Schemer very much. I might take a look at it next month.
    - nextos 11y ago
      As to comparability of those books, well, I asked because theorem proving is the most general approach (vs abstract interpretation, data/control flow analysis, model checking and type systems). So I was wondering if Software Foundations referred to these, so it could be regarded as a intro book which could then be followed up by [1-3]. I think I disagree a bit wrt model checking, which is very useful in some specialized domains. I have had quite a lot of success with it when verifying complex real time systems, specified as timed automata. We then generated code from this specifications. It'd be challenging to use any other technique to achieve such an exhaustive verification. Both [1-2] can be found online, and [2] is particularly enlightening! I followed a course by the authors, and implemented a big chunk of the book. It's really awesome to implement static analyzers by interpreting programs with a more abstract set of types.
auggierose 11y ago
Looks like the book should have been called 'Playing with Coq' instead.
- coolsunglasses 11y ago
  Is there some better resource for learning programs-are-proofs people should be using?
  - auggierose 11y ago
    In my opinion, many people are curry Howard blind. It's like they found this one correspondence between certain proofs (constructive ones) and programs and are hell-bend on using it. Personally I like not to confuse the two things. Proofs are proofs, programs are programs, programs can generate proofs, proofs can verify programs. And proofs are classical.
    - mafribe 11y ago
      Identifying proofs with programs undeniably gives a beautiful economy of concepts, best experienced among mature tools maybe in Agda. But there is a price to be paid, and that's the restriction to constructive logic. If you need classical logic, use an LCF-style prover like Isabelle/HOL.
      - pron 11y ago
        > But there is a price to be paid, and that's the restriction to constructive logic. That's the price on the proof side. The price on the program side is the need to encode complexity in the types because C-H is about abstract programs, not computations. Otherwise, the existence of a computation is entirely ignored except where it may break the logic's consistency in the case of non-termination, but from the computation's perspective, a long computation and a non-terminating one are the same. The result is that you can "prove" the correctness of programs that are effectively non-computable, i.e. programs that don't encode effective computations (by effective computation I mean one that terminates before the end of the universe, but it could be exchanged with more practical definitions).
krat0sprakhar 11y ago
Can someone familiar with this kind of stuff lay out a few benefits of learning this material for a practicing programmer? I'm quite interested (since I've heard a lot about Coq and Pierce) but since there are so many things to learn, I want to prioritize appropriately.
- tel 11y ago
  It's hard to say exactly. It will teach you to think of programming in an entirely new way. Will that make it easier to write good code elsewhere? Almost certainly if you're not familiar with mathematical proof (maybe you took a discrete math course before). If you know what it is to prove then you'll learn an interesting deep connection between programming and proving. You probably don't want to prove things in your programs. Not really. Even after you learn Coq it's too difficult to do day-to-day. But proofs do not work without being completely consistent in the same way that good programs are. So you can learn a lot of techniques for good programs from techniques for good proofs. Coq rejects bad proofs, so it can be good practice. Finally, Coq is unashamedly higher-order. The chops you gain working with it will translate more or less directly to better functional programming comprehension.
- nextos 11y ago
  I moved to Scandinavia and got a MSc which was very strong in formal methods: static analysis, model checking and theorem proving; some big names in the field teaching there. I was able to access highly technical programming jobs, those where you are using formal or semi-formal methods to build critical and/or real-time systems. These are very well paid and very nice to work on. You end up designing and implementing very elegant systems with nice guarantees. It feels like high-end engineering. So from a pragmatic point of view, you can access better jobs. From a more idealistic perspective, you will understand computation better.

95 points by nextos 11y ago

Pils 11y ago

Working through this right now as a directed reading with a professor and a couple of other students. Would definitely recommend this as a follow up to an intro PL course.

bkase 11y ago

Certified Programming with Dependent Types (available online as well http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/) is also a good resource for learning Coq (note: I just started working through the material this weekend).

javajosh 11y ago

Uh, how do you pronounce Coq?

cmrx64 11y ago
https://translate.google.com/#fr/en/coq https://translate.google.com/#fr/en/coq, click "listen". Or, in French IPA (https://en.wikipedia.org/wiki/Help:IPA_for_French https://en.wikipedia.org/wiki/Help:IPA_for_French), kɔk (roughly transcribed to English, "couk") But, everyone I know (including me) who I've heard pronunce it just pronunces it "cock".
tel 11y ago
As is traditional: You pronounce it with an understanding of how difficult it must be to speak French and have most of the CS world talk about bit twiddling.
- pron 11y ago
  :)

davidgrenier 11y ago

Whatever your views on that stuff... it is fun to play in Coq. On the other hand, playing with J-Bob, the toy "proof assistant" used in The Little Prover is tedious at best. I'm torn between just giving up with the last two chapters of the book undone.

cmrx64 11y ago

This is a lovely book. I gathered a group of students to work through this book last year (and even roped in a professor). If you're interested in formal software verification or interactive proof assistants, this is an excellent and approachable introduction. Another free book, using the Isabelle proof assistant, is http://concrete-semantics.org/ http://concrete-semantics.org/. It's also very good.

nextos 11y ago
It looks very nice. The Little Prover, recently published is also a neat small intro. I wonder how does Software Foundations compare against other more specialized classics in the field like [1-3]. [1] https://mitpress.mit.edu/books/principles-model-checking https://mitpress.mit.edu/books/principles-model-checking [2] http://www.springer.com/fr/book/9783540654100 http://www.springer.com/fr/book/9783540654100 [3] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/
- cmrx64 11y ago
  I've worked through TaPL too. I'm not even sure they are comparable :) It's possible to formalize the contents of TaPL in these systems (and, indeed, Pierce has taught it like that). But it's still a very different focus than Software Foundations. I've not read or worked through the other books (wow they are expensive), but I'm in general not very keen on model checking as an approach. Tools like Alloy or NuSMV can be useful when designing or investigating algorithms, but they always do a bounded search and can't be applied directly to implementations. I personally don't confer that much trustworthyness to systems that appeal to model checking tools for their correctness. I've seen The Little Prover, but am somewhat wary of it. On the other hand, I enjoyed The Little Schemer very much. I might take a look at it next month.
  - nextos 11y ago
    As to comparability of those books, well, I asked because theorem proving is the most general approach (vs abstract interpretation, data/control flow analysis, model checking and type systems). So I was wondering if Software Foundations referred to these, so it could be regarded as a intro book which could then be followed up by [1-3]. I think I disagree a bit wrt model checking, which is very useful in some specialized domains. I have had quite a lot of success with it when verifying complex real time systems, specified as timed automata. We then generated code from this specifications. It'd be challenging to use any other technique to achieve such an exhaustive verification. Both [1-2] can be found online, and [2] is particularly enlightening! I followed a course by the authors, and implemented a big chunk of the book. It's really awesome to implement static analyzers by interpreting programs with a more abstract set of types.

auggierose 11y ago

Looks like the book should have been called 'Playing with Coq' instead.

coolsunglasses 11y ago
Is there some better resource for learning programs-are-proofs people should be using?
- auggierose 11y ago
  In my opinion, many people are curry Howard blind. It's like they found this one correspondence between certain proofs (constructive ones) and programs and are hell-bend on using it. Personally I like not to confuse the two things. Proofs are proofs, programs are programs, programs can generate proofs, proofs can verify programs. And proofs are classical.
  - mafribe 11y ago
    Identifying proofs with programs undeniably gives a beautiful economy of concepts, best experienced among mature tools maybe in Agda. But there is a price to be paid, and that's the restriction to constructive logic. If you need classical logic, use an LCF-style prover like Isabelle/HOL.
    - pron 11y ago
      > But there is a price to be paid, and that's the restriction to constructive logic. That's the price on the proof side. The price on the program side is the need to encode complexity in the types because C-H is about abstract programs, not computations. Otherwise, the existence of a computation is entirely ignored except where it may break the logic's consistency in the case of non-termination, but from the computation's perspective, a long computation and a non-terminating one are the same. The result is that you can "prove" the correctness of programs that are effectively non-computable, i.e. programs that don't encode effective computations (by effective computation I mean one that terminates before the end of the universe, but it could be exchanged with more practical definitions).

krat0sprakhar 11y ago

Can someone familiar with this kind of stuff lay out a few benefits of learning this material for a practicing programmer? I'm quite interested (since I've heard a lot about Coq and Pierce) but since there are so many things to learn, I want to prioritize appropriately.

tel 11y ago
It's hard to say exactly. It will teach you to think of programming in an entirely new way. Will that make it easier to write good code elsewhere? Almost certainly if you're not familiar with mathematical proof (maybe you took a discrete math course before). If you know what it is to prove then you'll learn an interesting deep connection between programming and proving. You probably don't want to prove things in your programs. Not really. Even after you learn Coq it's too difficult to do day-to-day. But proofs do not work without being completely consistent in the same way that good programs are. So you can learn a lot of techniques for good programs from techniques for good proofs. Coq rejects bad proofs, so it can be good practice. Finally, Coq is unashamedly higher-order. The chops you gain working with it will translate more or less directly to better functional programming comprehension.
nextos 11y ago
I moved to Scandinavia and got a MSc which was very strong in formal methods: static analysis, model checking and theorem proving; some big names in the field teaching there. I was able to access highly technical programming jobs, those where you are using formal or semi-formal methods to build critical and/or real-time systems. These are very well paid and very nice to work on. You end up designing and implementing very elegant systems with nice guarantees. It feels like high-end engineering. So from a pragmatic point of view, you can access better jobs. From a more idealistic perspective, you will understand computation better.