6 ms·
The Little Prover
- drcode 11y agoI've had the pleasure of reading a pre-release version of this book and enjoyed it immensely [1]. Yes, it's true most of us will probably never need to write mathematically-provable software [2] but it's still good to know WHY we don't do this for our day-to-day programming, by getting a feel for just how challenging it is to do this. However, I'm no expert on writing provably-true software, so take my opinion with a grain of salt... you may want to wait for reviews from experts in this field who can compare this book to other alternatives. [1] Note that the "Little X" series of books have a peculiar style and may not be to everyone's taste. I'm speaking as someone who enjoyed all of the previous books in this series immensely. [2] Although programmatic proofs may start becoming more mainstream in the future: For instance, with "smart contracts" they may play a major role, and are already planned as a feature for the ethereum solidity smart contract language... Not surprisingly, if you are handling currency in a contract, people like to know things like "There is no scenario in which the other party can run away with all my money".
- surganov 11y agoTo me it's like Star Wars VII.
- davexunit 11y agoI know nothing about the subject, but I love this series. Going to drop by MIT Press when I get the chance and pick it up.
- pykello 11y agoReading this news while self-studying and enjoying the "Software Foundations" [1] course is so sweet. [1] http://www.seas.upenn.edu/~cis500/current/index.html http://www.seas.upenn.edu/~cis500/current/index.html
- picardo 11y agoIs there an ebook version somewhere?
- JadeNB 11y agoIt looks like it's an introduction to by-hand proofs about software, rather than to software-assisted proofs. That's a shame—I got very excited at the thought of a 'Little X' take on proof assistants!
- JadeNB 11y agoSometimes I can understand downvotes in retrospect, but that one puzzles me. I thought that it was a constructive contribution for others who had the same expectation that I did. Was it actually not? Should I just not have said anything, or should I have phrased it differently?
- nmrm2 11y agoWasn't me, but you might've been downvoted because the book description states: The book comes with a simple proof assistant to help readers work through the book and complete solutions to every example. So, there is a proof assistant.
- JadeNB 11y agoThanks for this helpful clarification; I hadn't noticed that in the description. (I do note, feebly, that there's a difference between learning to use a one-off proof assistant, and learning to use a 'popular' one.)
- WaxProlix 11y agoMy girlfriend and I are starting to play around with proof assistants (avoiding the coq joke as best I can...) and it would be great to have something like this to go along with that endeavour.
- pykello 11y agoWhich proof assistants did you play with? Why are avoiding coq?
- pkrumins 11y agoOmg omg omg. I haven't been this excited about a book release for a long time. I just preordered this book. I can't wait to go through it cover to cover.
- eli_gottlieb 11y agoOh hey, they're writing a PLT Group rival to Software Foundations and Certified Programming with Dependent Types.
- sriram_sun 11y agoI worked out every problem in The Little Schemer back in 2000 with only a C++ programming and no computer science background. It was very approachable and my only source of joy in a nightmarish academic setting. I am looking forward to this book with the same degree of enthusiasm :)!
- psibi 11y agoCan I see the table of contents anywhere ?