HN Books @HNBooksMonth

For those who want to see Dijkstra's mathematics of programs in action:

1) basic (great for kids, math novices, whatever): https://www.amazon.com/gp/product/0470684534/ref=dbs_a_def_r... (ignore the two star review, this book would get 5 stars from me)

2) advanced (free, complete with videos): http://www.cs.toronto.edu/~hehner/aPToP/

3) advanced: https://www.amazon.com/gp/product/0470848820/ref=dbs_a_def_r...

4) advanced, theoretical, from the man himself: https://www.springer.com/gp/book/9781461279242

⬐ madhadron

I learned this stuff from Roland's 'Program Construction'. Great book. Once you've been through that, then suddenly Dijkstra's writing becomes really practical.

⬐ User23

Also advanced, but quite readable: https://www.amazon.com/Discipline-Programming-Edsger-W-Dijks...

⬐ jonsen

Ad 1) Two five-star reviews on amazon UK:

https://www.amazon.co.uk/Algorithmic-Problem-Solving-Roland-...

⬐ jonsen

5) advanced: https://www.amazon.com/Science-Programming-Monographs-Comput...

⬐ mcguire

Also, slightly less advanced:

A Discipline of Programming

https://www.amazon.com/Discipline-Programming-Edsger-W-Dijks...

For more practical fun, consider Frama-C, SPARK, and Dafny.

E. Hehner has a course called "Formal Methods for Software Design", which he presents completely openly online (including video lectures, a textbook, solutions, and so on): http://www.cs.toronto.edu/~hehner/FMSD/

I really liked it.

I also liked R. Backhouse's approach to it, encapsulated in two books:

1) less playful: http://www.amazon.com/Program-Construction-Calculating-Imple...

2) more playful: http://www.amazon.com/Algorithmic-Problem-Solving-Roland-Bac...

If you are looking for motivation, you might also like: http://research.microsoft.com/en-us/um/people/lamport/pubs/p...

-----------------

I found Dijkstra's stuff to be easier to read after I had read books by Hehner/Backhouse, even though chronologically, Dijkstra came first.

⬐ nickpsecurity

Hehner's work is on my reading list. The reviews on Backhouse's links aren't promising.

⬐ bmer

I have learned not to put much weight in Amazon reviews for technical literature. Borrow a copy of the books from a library (my city library actually had access to a digital version of Backhouse's latest book, and you could always Yarr! yourself a copy) and check them out, before shelling out the cash :)

⬐ nickpsecurity

Well, the one reviewer said it was only a start toward a method for practical software with practical part maxing out at a sorting algorithm. Is that true or do you have examples of realistic stuff covered by book?

⬐ bmer

Backhouse's more playful book, focuses primarily on teaching one how to write and use proofs in the "calculational style" of Dijkstra/Hoare/Lamport/others.

Backhouse's less playful book covers the same topic, but has some more programming examples:

* cyclic code error correction * simple sorting algorithms * real number to integer conversion is used to introduce Galois connections

Again, this isn't a lot in terms of "practical examples". No production level software is built here. If you're looking for that sort of stuff, maybe you want to try out L. Lamport's book: http://www.amazon.com/Specifying-Systems-Language-Hardware-E...

I haven't read that book though.

⬐ nickpsecurity

Anyone that knows about all these resources should really scour them to put together a list of their application to real-world problems. Any researchers that like the stuff should apply them to real-world problems. The reason is that we don't know if such methods are a waste of time or useful until that happens. So, I'm interested in anything you have on that.

EDIT: Your recommendation was good as it clearly has practical advice. I can tell just looking at table of contents. And, as a gift, I found the whole book for free plus other things in link below. :)

http://research.microsoft.com/en-us/um/people/lamport/tla/bo...

⬐ Cyph0n

Thank you for linking that course. I've always been interested in formal methods and verification of correctness.

⬐ bmer

No problem. You'll notice as you go through the links that none are about verification of correctness. Rather, they are about "correct by construction".