Hacker News Reader

Comment by mcmancini | Hacker News Reader

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.

View on HN

Software Foundations 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.

Winner winner chicken dinner.

I read the preface and this sounds exactly like what I was looking for. Many thanks!

I worked through it last year and had a great time. Enjoy!

I've heard good things about Certified Programming with Dependent Types (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_depend....

I could recommend Coq Art: 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.

Reply on news.ycombinator.com