I quite enjoyed Tony Hoare's essay - thanks for sharing. A lot of what he wrote has stood the test of time!

Re: Hoare logic; Precondition, Command, Postcondition: https://news.ycombinator.com/item?id=47335703

"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

how are people currently evaluating between the different spec writing frameworks out there?

"load-bearing" - lol, nice easter egg. no one likes the AI-isms in writing!

Pretty good point - I would actually argue that the imperative nature of prompting takes some of the blame here too. Your initial goal gets "steered" by the agent system and follow-up messages take precedence.