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/
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/