(566e) Writing Bug-Free Software Using Lean

When developing new methods for molecular simulation, eliminating bugs can be challenging. Programming languages like Python, FORTRAN, and Julia flag syntax errors, but don't (and cannot) catch errors in math or program logic - these must be rooted out by human experts. These issues can be managed by following best practices in software development (such as writing tests alongside the program), but even these do not guarantee that code is correct.

Lean is a new programming language developed for writing and automatically checking the logic of math proofs. We show how Lean can be used to write programs in scientific computing, and report on our progress toward writing a molecular dynamics simulation engine, and proving its correctness, in Lean.