I found out about this text from Omega Tau podcast 243: http://omegataupodcast.net/243-formal-specification-and-proof/