Thirteenth Summer School on Formal Techniques

For the last week and a half I’ve been at the Thirteenth Summer School on Formal Techniques. It has been a great experience as a newer PhD student which I would highly recommend to anyone even tangentially interested in formal methods. This will be a short post just pointing out a few talks that stood out to me.

Firstly, it was an absolute treat to meet Leonardo de Moura and David Thrane Christiansen. Leo spoke at some length about the Lean Focused Research Organization (FRO), which I think has thoughtfully assembled a focused roadmap that will provide the language with great inroads towards further usability and longevity. I was especially pleased to see the documentation tool Verso that David is working on. This tools borrows ideas from Alectryon, allowing you to write literate Lean code that that can be exported into something like a website or textbook, with the wonderful feature of being able to see intermediate proof states. While this project is in an early stage, it is already being used on the Lean blog, and I am excited to see its continued development.

David also led some practical labs with what I felt was a well-crafted repo of exercises. It walks through the perhaps familiar exercises of verifying optimizations for a small imperative language embedded in Lean, but with some fun deviations such as using Lean’s metaprogramming to set up quasiquoting and using LeanSAT to automate a long computational proof. My impression was that David has a keen eye towards appropriate pedagogy for proof assistant beginners and an infectious sense of joy found in doing so. I could not imagine another person more well-suited to work on the documentation goals that the Lean FRO has developed.

We also had a chance to speak with Chris Lattner, know for his work on projects such as the development of LLVM, Swift, and most recently the Mojo programming language. If you’ve not previously heard of Mojo, it is a programming language that aspires to be a superset of Python with additional features such as linear types and compilation that is intended to for instance be well-suited to code running on GPUs, with an eye towards AI applications. While I am not particularly interested in these applications, I think any work from a respected compiler developer that aims to bridge the increasing gap between high-level languages and hardware-aware programming is worth keeping an eye on.

The last piece of research I’ll mention is from Armando Solar-Lezama. Again, while I am not acutely interested in AI or Python, I did find some interest his research that connects program synthesis with AI. To avoid the risk of poorly explaining something outside my research area, I’ll be brief. The core idea appears to be first specifying the grammar of a DSL, then treating programs (with a focus on numeric matrices) as differentiable structures. From there the idea is to first learn an architecture, then fine tune these architectures with additional training. As an example, during a lab exercise I was able to find a decent approximation to a program for simulating a bouncing ball using the newly released neurosym-lib. While I retain my healthy skepticism towards AI in formal methods applications, I feel that this approach of users constraining the type of programs produced is a step towards the kind of guardrails that would provide me with a bit more comfort.

Thank you to Natarajan Shankar and the many other speakers of the summer school for putting this together!