| ▲ | lkuty a day ago | |
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 | ||