I quite enjoyed Tony Hoare's essay - thanks for sharing. A lot of what he wrote has stood the test of time!
"Three ways formally verified code can go wrong in practice" re: Hoare logic and DbC Design-by-Contract patterns: https://news.ycombinator.com/item?id=45562815