Abstract: Software design is when you try to figure out how a solution to a given problem should work and, crucially, how to verify that such a solution (if it exists) is what it claims to be. We will discuss why this verification step is so important and remark that there could be no essential distinction between verifying a piece of mathematics and verifying the correctness of a software solution. We will describe an approach to formal verification using Lean. [Lean](Link identifier #identifier__108809-1https://lean-lang.org/) is a 10+ years old project well-known for its vibrant community and its efforts in formalization of wide areas of mathematics. Lean started as an interactive theorem prover and evolved into a powerful (and wonderful) programming language. We will discuss Lean, primarily as a programming language.
This post is also available in: Link identifier #identifier__171592-5Eng