Ordinateur
A blog about software engineering, by Brent S.
Latest Post:
I Proved Leftpad
I’ve been orbiting around the concept of formal methods AKA formal verification AKA automated reasoning for a few years now. This year I’ve come up with a more concrete plan to study the topic from the ground up. When reading an early release of Hillel Wayne’s book Logic for Programmers, I learned about the project Let’s Prove Leftpad. The Verus verification framework has been a hot topic at work over the past year so I decided to give it a try on a fairly straightforward proof.