4 ms·

Is there a good practical resource for learning about applying formal proof systems like Coq or Spin, but for those without a CS background? I'm interested in p

Is there a good practical resource for learning about applying formal proof systems like Coq or Spin, but for those without a CS background? I'm interested in provably correct systems, but a lot of the material seems to be heavy on the theoretical side. I guess you could say I'm searching for the Art of Electronics, but for formal proofs.

seanwilson 12y ago
I could recommend Coq Art: http://www.labri.fr/perso/casteran/CoqArt/ http://www.labri.fr/perso/casteran/CoqArt/ Unfortunately, formal proofs are very theoretical and there's a lot of concepts to learn that aren't found in regular programming. This book eases you into things though.
adultSwim 12y ago
Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html To my knowledge it's the most accessible book/class/tutorial on Coq. Starts off slowly and has a lot of interactive examples. Suitable for self-study. Comparing with what else is out there, really shows how refined and well-tested it is. Highly recommend.
- mcmancini 12y ago
  Winner winner chicken dinner. I read the preface and this sounds exactly like what I was looking for. Many thanks!
  - eli_gottlieb 12y ago
    I worked through it last year and had a great time. Enjoy!
pseudonom- 12y ago
I've heard good things about Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/). "This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation." Edit: There's some comparison of CPDT and SF here: https://lobste.rs/s/c3lj14/certified_programming_with_dependent_types_by_adam_chlipala https://lobste.rs/s/c3lj14/certified_programming_with_depend....

seanwilson 12y ago

I could recommend Coq Art: http://www.labri.fr/perso/casteran/CoqArt/ http://www.labri.fr/perso/casteran/CoqArt/ Unfortunately, formal proofs are very theoretical and there's a lot of concepts to learn that aren't found in regular programming. This book eases you into things though.

adultSwim 12y ago

Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html To my knowledge it's the most accessible book/class/tutorial on Coq. Starts off slowly and has a lot of interactive examples. Suitable for self-study. Comparing with what else is out there, really shows how refined and well-tested it is. Highly recommend.

mcmancini 12y ago
Winner winner chicken dinner. I read the preface and this sounds exactly like what I was looking for. Many thanks!
- eli_gottlieb 12y ago
  I worked through it last year and had a great time. Enjoy!

pseudonom- 12y ago

I've heard good things about Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/). "This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation." Edit: There's some comparison of CPDT and SF here: https://lobste.rs/s/c3lj14/certified_programming_with_dependent_types_by_adam_chlipala https://lobste.rs/s/c3lj14/certified_programming_with_depend....