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 ma

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