Day 4 -

Aug 21st

Creative and Mix

16:10 - 16:50

How to write correct Scala programs

Scala, because of its functional nature, already gives us some design tools to write correct programs: type polymorphism, higher-order functions, immutability, and others. There are also many test frameworks that allow us to detect some bugs. This is a good start, but we can do more: proving the absence of bugs. In this talk I will show how to use Isabelle, a proof assistant, to implement algorithms, prove them correct, and compile them as Scala programs. We’ll see how to formulate universal properties on programs and how to check them.

Lars Hupel

Giesecke+Devrient

Lars is an Evangelist at Giesecke+Devrient, a security technology company. An engineer at heart, they are working to bring modern financial services to people. Lars writes articles and talks about a multitude of topics. Previously, Lars was a PhD student at TU München in the field of logic and verification. Their research focus was on techniques for verified code generation from theorem provers.

Subscribe

Join our conference

Subscribe and follow @ScalaDays on BlueSky for the latest conference updates.