5 ms·

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

• rramadass 6mo 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 6mo ago
    Rediscovering it through the Dafny programming language. Brings back memories of a 1994 University course.
    • rramadass 6mo ago
      You might find this paper interesting (uses examples in Dafny) - https://news.ycombinator.com/item?id=47334375 https://news.ycombinator.com/item?id=47334375
    • rramadass 6mo ago
      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 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/