Yes, but don't forget his formal work also (Hoare logic).

To me, this is his most important contribution; Everybody else built on top of this.

Rediscovering it through the Dafny programming language. Brings back memories of a 1994 University course.

	▲	rramadass a day ago \| parent \| next [-]
		I think it is even more relevant today. Hoare Logic + Dijkstra's weakest precondition + Meyer's Design-by-Contract is what should be used to get LLMs to generate proof with code in a correctness-by-construction approach to implementation. References: Correctness-by-Construction (CbC) - https://www.tu-braunschweig.de/en/isf/research/cbc A Course on Correctness by Construction - https://wp.software.imdea.org/cbc/
	▲	rramadass 5 hours ago \| parent \| prev [-]
		You might find this paper interesting (uses examples in Dafny) - https://news.ycombinator.com/item?id=47334375