News for hackers. Stuff that matters.

A comment on Coming Soon: Machine-Checked Proofs in Everyday Development.

Re:Coming Soon: Machine-Checked Proofs in Everyday Development by haskellandchill on Saturday December 30, 2017 @06:08PM (#16038252)
My current reading list:

- Fundamental Proof Methods in Computer Science

- Handbook of Practical Logic and Automated Reasoning

- Software Abstractions

- The Little Prover

Yes, currently I have Athena, OCaml, Alloy, ACL2 (via Dr Racket/Dracula) all up and running to work through the exercises in these books. I'm very skeptical anything will come of this, but it interests me and I can see the value.

Hopefully the speaker's next book Formal Reasoning About Programs (https://github.com/achlipala/frap) will be a nice next step, I have Certified Programming with Dependent Types but have not cracked it yet. Also keeping an eye on Verified Functional Algorithms (https://softwarefoundations.cis.upenn.edu/vfa-current/index....).

[ Parent | on HN ]
Re:Coming Soon: Machine-Checked Proofs in Everyday Development by meneame2 on Saturday December 30, 2017 @09:03PM (#16038918)
Three extra classics:

* https://books.google.es/books?id=YseqCAAAQBAJ

* http://www.concrete-semantics.org/

* https://softwarefoundations.cis.upenn.edu/

[ Parent | on HN ]
Re:Coming Soon: Machine-Checked Proofs in Everyday Development by adultSwim on Wednesday January 03, 2018 @11:37AM (#16062430)
+1 for Software Foundations
[ Parent | on HN ]
Re:Coming Soon: Machine-Checked Proofs in Everyday Development by abecedarius on Saturday December 30, 2017 @07:15PM (#16038492)
> The Little Schemer

Do you mean The Little Prover?

[ Parent | on HN ]
Re:Coming Soon: Machine-Checked Proofs in Everyday Development by haskellandchill on Saturday December 30, 2017 @07:18PM (#16038504)
Yes! Thanks.
[ Parent | on HN ]