Seminario Crittografia: Mathematical proofs in software design

Lunedì 6 Maggio 2024 alle ore 14.30, presso il Dipartimento di Matematica e Fisica (Via della Vasca Navale, 84 - Aula 108), il dottor Marcello Paris (UniCredit) nell'ambito dei Seminari di Crittografia, terrà il seminario dal titolo "Mathematical proofs in software design".

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](https://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.