Stream: Program verification
Дмитрий Лейкин (Nov 24 2020 at 17:03):
I'm software developer. Is there any examples of program verification using Lean, or tutorials, that can be used for learning? Not to prove theorems about math, but theorems about code to prove it's correctness? Now I found only https://kqueue.org/blog/2020/10/15/arithcc/ (which was very helpful for learning).
Anne Baanen (Nov 24 2020 at 17:09):
We're teaching a course on formal verification in Lean at the moment :)
Johan Commelin (Nov 24 2020 at 17:14):
@Дмитрий Лейкин Also note that Lean 4 will probably make program verification a lot more pleasant compared to Lean 3.
Last updated: May 08 2021 at 22:13 UTC