The Little Prover | Hacker News Reader

The Little Prover

mitpress.mit.edu

135 pointsnickmain20 comments

I'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".

It 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!

Sometimes 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?

Wasn'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.

Thanks 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.)

My 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.

Which proof assistants did you play with? Why are avoiding coq?

I think WaxProlix (https://news.ycombinator.com/item?id=9553471) was avoiding puerile jokes about (a homonym for) Coq, not avoiding Coq itself.

Yes, exactly, especially in the context of "my girlfriend and I", "playing with", etc. Low-(brow|hanging fruit), even for me.

I liked Coq d'Art

Reading 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

Omg 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.

Oh hey, they're writing a PLT Group rival to Software Foundations and Certified Programming with Dependent Types.

To me it's like Star Wars VII.

I 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 :)!

I 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.

Note the target release is in July, lest you be disappointed this weekend. Not that the MIT Press shop could actually be disappointing...

Thanks for sparing me from being dumb and going into the store tonight.

Can I see the table of contents anywhere ?

Is there an ebook version somewhere?

Reply on news.ycombinator.com