"When the going gets tough, the tough get proving"
A talk by Dr. Jesse Alama (Igalia, Germany/Spain)
Main content
The talk starts at 13:00, coffee will be served from 12:45. Please help us cut down waste by bringing your own mug.
Abstract:
We all know that software testing of various stripes can help your check that your program is correct. A comprehensive test suite can indeed give us a lot of confidence in our code. But when the code gets just a bit too tricky, or when it's mission-critical to make sure that you're getting the details right, or when you're working with pseudocode that cannot actually be run, another approach to gaining confidence in our work arises: proving mathematical theorems about your programs. A variety of powerful tools can be used for this purpose.
In this talk, I'll show my recent work on adding exact decimal (base-10) arithmetic to the JavaScript programming language with the Lean interactive theorem prover. I'll explain how the process of adding new features to the JavaScript language works and why decimal arithmetic might be a bit more complex than it can appear, which will, I hope, demonstrate the value in reaching for power tools such as Lean.