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!
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.
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.
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.)
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.
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 :)!
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".