top | item 41076307 (no title) lucioperca | 1 year ago You can also verify software like compilers in Lean:https://aws.amazon.com/blogs/opensource/lean-into-verified-s... discuss order hn newest nextos|1 year ago Sure, but Lean has very little support for software problems compared to Isabelle, Coq or Dafny right now.Those 3 also have a lot of training data as well. Hoping Lean gets more support as it is very friendly.As a basic learning resource focused on software engineering, there's [1]. But nothing more advanced I am aware of.[1] The Hitchhiker's Guide to Logical Verification. https://cs.brown.edu/courses/cs1951x/static_files/main.pdf
nextos|1 year ago Sure, but Lean has very little support for software problems compared to Isabelle, Coq or Dafny right now.Those 3 also have a lot of training data as well. Hoping Lean gets more support as it is very friendly.As a basic learning resource focused on software engineering, there's [1]. But nothing more advanced I am aware of.[1] The Hitchhiker's Guide to Logical Verification. https://cs.brown.edu/courses/cs1951x/static_files/main.pdf
nextos|1 year ago
Those 3 also have a lot of training data as well. Hoping Lean gets more support as it is very friendly.
As a basic learning resource focused on software engineering, there's [1]. But nothing more advanced I am aware of.
[1] The Hitchhiker's Guide to Logical Verification. https://cs.brown.edu/courses/cs1951x/static_files/main.pdf