5 ms·

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 softwa

by 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.
    - cmrx64 11y ago
      Ah, I see what you mean. Software Foundation hints ever so slightly at more specific approaches. Looking into the other books a little bit more, I'm not so certain Software Foundations would serve as a good introduction to them. The reason being that it focuses very heavily on the theorem-proving aspects. Concrete Semantics, at least its second half, would be an excellent primer. Software Foundations puts more weight on proving properties about languages than it does verifying particular programs. Whereas Concrete Semantics culminates in Hoare logic and abstract interpretation. That sounds like an excellent use of model checking tools. Most approaches I've seen involve creating a model of some system separate from the implementation, which I think is risky. Still better than nothing, by far. I'll definitely have to check those books out now. Thanks for the recommendations!
      - nextos 11y ago
        Thanks for the Concrete Semantics recommendation!
  - pron 11y ago
    > and can't be applied directly to implementations There are model checkers that work directly on implementations, like NASA's JPF. > I personally don't confer that much trustworthyness to systems that appeal to model checking tools for their correctness. Given that the going rate for proofs is roughly 1-1.5 days per one line of code, which grows superlinearly with the code size, I think we have no choice... In any event, pretty much all safety-critical software that human lives depend on (even many, many lives) is verified with model-checking in the best case. Use of proofs in verifying safety-critical systems is very rare, as even those domains can rarely afford it. Also, remember that no one really needs 100% proof, as no other, non-software component in the system guarantees 100% reliability (not that model-checking can give us probability bounds).
    - tel 11y ago
      100% certainty in proof doesn't mean that you're aiming to get a 100% proven system. It means that you can stop worrying about the proven part forevermore. So it reduces long term running overhead.
      - pron 11y ago
        If your proven component is so well-isolated from others and doesn't undergo changes (and neither do its assumptions about input), it seems like the same would apply to a model-checked component. Besides, the cost of proofs is well over 1Kx if not 10Kx over model checking, so I don't see how this consideration is important. Proofs are useful -- because of their total coverage -- when verifying components that will be used in many different projects, like compilers, kernels and libraries, and even then only when they are sufficiently small to be doable within, say, 5-10 years by a dedicated team. A one-time gigantic job will pay for itself by being used (and hopefully paid for) by many customers over many years.
        tel 11y ago
        I've got no problem with model checkers, though I'm not sure I agree with your effort ratings. Different tools for different jobs, eh? I think I also have a different conception of proof than you're naming. You don't need to prove your entire program. 10 small proofs strung together can go an enormous distance with low weight.
- coolsunglasses 11y ago
  >The Little Prover, recently published is also a neat small intro. Really? I know a lot of programmers that were excited for TLP and were very disappointed. I haven't even gotten a lukewarm review from anyone yet.
  - nextos 11y ago
    Well, it's OK. I don't like any of the Little books or HtDP that much except The Little Schemer (neé as The Little Lisper).
mafribe 11y ago
I'm thinking of doing something similar with my PhD students who have no backgroud in maths, but are strong programmers. How did you organise reading such a book? Any recommendations? I wonder if I should go Isabelle, Coq or Agda. The former is more suitable to my personal prover needs, as I like classical logic and nominal techniques, but I have a feeling that Coq is easier to get into because there is more literature. Agda is the cleanest system, but lacks proof automation.
- cmrx64 11y ago
  We were a group of mostly undergrads. Computer Science students. What we did was meet once a week to discuss the reading and the exercises, or work through the exercises together. During the week we'd read the next few sections and try the exercises. Especially at first it was really slow and took a lot of effort as we weren't very comfortable with that form of logic (most of us had only previously taken an undergrad intro to discrete math class). I personally like Isabelle very much, and if I were to start this with a new group of people I'd do it in Isabelle. Its Prover IDE in the form of Isabelle/jEdit is much nicer than Proof General or CoqIDE. I also think its presentation is a bit more immediately understandable for someone familiar with classical logic but not necessarily type theory. Isabelle/HOL is very natural from that perspective, imo.
  - mafribe 11y ago
    Thanks. I agree that Isabelle's jEdit integration is nice. But what would be a polished and up-to-date introduction? I think "Concrete Semantics" is a bit heavy going for a complete beginner. No detailed explanation of proof rules, tactics etc.
    - cmrx64 11y ago
      Isabelle's tutorial is quite comprehensive, and, I think, rather approachable to an ITP beginner: http://isabelle.in.tum.de/dist/Isabelle2015/doc/tutorial.pdf http://isabelle.in.tum.de/dist/Isabelle2015/doc/tutorial.pdf It assumes some knowledge of basic functional programming, but builds up proving-related jargon quite quickly through examples with some interspersed explanations. It doesn't discuss structured proofs with Isar, and instead focuses on the tactical style, but I think this is an advantage - it's simpler that way, and structured proofs really only benefit human readers. They're somewhat confusing to write if you don't already have a good grasp of the entire system and what is possible. The length of that tutorial was really intimidating to me at first, but it's quite approachable and isn't all that dense. It does take some time to work through it enough to become comfortable with the system.

by cmrx64 11y ago

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.
  - cmrx64 11y ago
    Ah, I see what you mean. Software Foundation hints ever so slightly at more specific approaches. Looking into the other books a little bit more, I'm not so certain Software Foundations would serve as a good introduction to them. The reason being that it focuses very heavily on the theorem-proving aspects. Concrete Semantics, at least its second half, would be an excellent primer. Software Foundations puts more weight on proving properties about languages than it does verifying particular programs. Whereas Concrete Semantics culminates in Hoare logic and abstract interpretation. That sounds like an excellent use of model checking tools. Most approaches I've seen involve creating a model of some system separate from the implementation, which I think is risky. Still better than nothing, by far. I'll definitely have to check those books out now. Thanks for the recommendations!
    - nextos 11y ago
      Thanks for the Concrete Semantics recommendation!
- pron 11y ago
  > and can't be applied directly to implementations There are model checkers that work directly on implementations, like NASA's JPF. > I personally don't confer that much trustworthyness to systems that appeal to model checking tools for their correctness. Given that the going rate for proofs is roughly 1-1.5 days per one line of code, which grows superlinearly with the code size, I think we have no choice... In any event, pretty much all safety-critical software that human lives depend on (even many, many lives) is verified with model-checking in the best case. Use of proofs in verifying safety-critical systems is very rare, as even those domains can rarely afford it. Also, remember that no one really needs 100% proof, as no other, non-software component in the system guarantees 100% reliability (not that model-checking can give us probability bounds).
  - tel 11y ago
    100% certainty in proof doesn't mean that you're aiming to get a 100% proven system. It means that you can stop worrying about the proven part forevermore. So it reduces long term running overhead.
    - pron 11y ago
      If your proven component is so well-isolated from others and doesn't undergo changes (and neither do its assumptions about input), it seems like the same would apply to a model-checked component. Besides, the cost of proofs is well over 1Kx if not 10Kx over model checking, so I don't see how this consideration is important. Proofs are useful -- because of their total coverage -- when verifying components that will be used in many different projects, like compilers, kernels and libraries, and even then only when they are sufficiently small to be doable within, say, 5-10 years by a dedicated team. A one-time gigantic job will pay for itself by being used (and hopefully paid for) by many customers over many years.
      - tel 11y ago
        I've got no problem with model checkers, though I'm not sure I agree with your effort ratings. Different tools for different jobs, eh? I think I also have a different conception of proof than you're naming. You don't need to prove your entire program. 10 small proofs strung together can go an enormous distance with low weight.
coolsunglasses 11y ago
>The Little Prover, recently published is also a neat small intro. Really? I know a lot of programmers that were excited for TLP and were very disappointed. I haven't even gotten a lukewarm review from anyone yet.
- nextos 11y ago
  Well, it's OK. I don't like any of the Little books or HtDP that much except The Little Schemer (neé as The Little Lisper).

mafribe 11y ago

I'm thinking of doing something similar with my PhD students who have no backgroud in maths, but are strong programmers. How did you organise reading such a book? Any recommendations? I wonder if I should go Isabelle, Coq or Agda. The former is more suitable to my personal prover needs, as I like classical logic and nominal techniques, but I have a feeling that Coq is easier to get into because there is more literature. Agda is the cleanest system, but lacks proof automation.

cmrx64 11y ago
We were a group of mostly undergrads. Computer Science students. What we did was meet once a week to discuss the reading and the exercises, or work through the exercises together. During the week we'd read the next few sections and try the exercises. Especially at first it was really slow and took a lot of effort as we weren't very comfortable with that form of logic (most of us had only previously taken an undergrad intro to discrete math class). I personally like Isabelle very much, and if I were to start this with a new group of people I'd do it in Isabelle. Its Prover IDE in the form of Isabelle/jEdit is much nicer than Proof General or CoqIDE. I also think its presentation is a bit more immediately understandable for someone familiar with classical logic but not necessarily type theory. Isabelle/HOL is very natural from that perspective, imo.
- mafribe 11y ago
  Thanks. I agree that Isabelle's jEdit integration is nice. But what would be a polished and up-to-date introduction? I think "Concrete Semantics" is a bit heavy going for a complete beginner. No detailed explanation of proof rules, tactics etc.
  - cmrx64 11y ago
    Isabelle's tutorial is quite comprehensive, and, I think, rather approachable to an ITP beginner: http://isabelle.in.tum.de/dist/Isabelle2015/doc/tutorial.pdf http://isabelle.in.tum.de/dist/Isabelle2015/doc/tutorial.pdf It assumes some knowledge of basic functional programming, but builds up proving-related jargon quite quickly through examples with some interspersed explanations. It doesn't discuss structured proofs with Isar, and instead focuses on the tactical style, but I think this is an advantage - it's simpler that way, and structured proofs really only benefit human readers. They're somewhat confusing to write if you don't already have a good grasp of the entire system and what is possible. The length of that tutorial was really intimidating to me at first, but it's quite approachable and isn't all that dense. It does take some time to work through it enough to become comfortable with the system.