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.
Which proof assistants did you play with? Why are avoiding coq?
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
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.)