Dijkstra and the origin of the XP-testing...

I was reading this (quite radical) paper from Dijkstra (1975),
http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD472.PDF

and at page 10 there is a very nice example of how to derive a function that computes the max of 2 values, using formal specifications.

It reminds me very much of the "test-first" approach of XP. I have to say that it looks the XP testing apporach really is the relaxed and less theoretical-heavy version of this.

Interesting how these ideas from the 70s keep coming back.