Zulip Chat Archive

Stream: Program verification

Topic: Examples


view this post on Zulip Дмитрий Лейкин (Nov 24 2020 at 17:03):

Hi Everyone,
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).

view this post on Zulip Anne Baanen (Nov 24 2020 at 17:09):

We're teaching a course on formal verification in Lean at the moment :)

view this post on Zulip 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