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.
Hoare Logic - https://en.wikipedia.org/wiki/Hoare_logic
Rediscovering it through the Dafny programming language. Brings back memories of a 1994 University course.
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/
To me, this is his most important contribution; Everybody else built on top of this.
Hoare Logic - https://en.wikipedia.org/wiki/Hoare_logic
Rediscovering it through the Dafny programming language. Brings back memories of a 1994 University course.
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/