3 ms·
To me, this is his most important contribution; Everybody else built on top of this. Hoare Logic - https://en.wikipedia.org/wiki/Hoare_logic https://en.wikiped
by rramadass 8mo ago
To me, this is his most important contribution; Everybody else built on top of this.
Hoare Logic - https://en.wikipedia.org/wiki/Hoare_logic https://en.wikipedia.org/wiki/Hoare_logic
- lkuty 8mo agoRediscovering it through the Dafny programming language. Brings back memories of a 1994 University course.
- rramadass 8mo agoI 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 https://www.tu-braunschweig.de/en/isf/research/cbc A Course on Correctness by Construction - https://wp.software.imdea.org/cbc/ https://wp.software.imdea.org/cbc/
- rramadass 8mo agoYou might find this paper interesting (uses examples in Dafny) - https://news.ycombinator.com/item?id=47334375 https://news.ycombinator.com/item?id=47334375