Theorem Prover Summer School

Two Week Summer School

• I have been attending a Summer School on Formal Methods for the past two weeks! It’s truly been amazing.
• I have a confession; I haven’t done any Computer Science things in a while, and I had a lot of anxiety once I found out there would be a fair number of Computer Science PhD students there. As it turns out, I would say it was about 80 percent CS people, and 20 percent Maths (Model Theory people, etc), with some people from industry (Nvidia, Sandia, etc) too. And it was exceptional.
• It was a very close-knit group, and even though we worked together, we also took a trip to San Francisco, did a hike at the Stanford Dish Trail and campus, did trips to various tech companies, the Computer History museum, and all the things (including several boba runs, movie night and games of Clue and Guess Who). In fact, it’s been so positive that a group of us will continue to learn one of the theorem provers together and continue to meet after the workshop ends, which is amazing!

As for the workshop

• The format was as such: in the first week, we had lectures in the morning, and labs in the afternoon (two each), where we were exposed to various Theorem Provers such as the Vampire Theorem prover, Alloy, PVS, and TPTP. TPTP has wonderful syntax, and Geoff’s website adds a delay to a random user if you don’t donate, which I thought was pretty funny. In one of my runs, I did get the delay, but I didn’t really notice, tbh.
• We honestly also got enough knowledge to build our own theorem prover, too, which is awesome and something maybe I do in the future (with more time, after my PhD).
• We had a lovely talk by Carolyn Talcott on McCarthy’s paper for its 60th birthday, and a session with Leslie Lamport on Paxos.
• We also did questions like a Soduku solver, and DDH using Easycrypt. Easycrypt looks interesting and definitely something I may put my hands on in the future, as it’s very applicable to some of the work I’m doing.

My purpose for attending

• I’m learning Lean in-depth this summer on my own, and am interested in using it as a tool for my work now and in the future. Firstly, mathematicians tend to like it, and it seems to have symbols that are very similar to stuff I’m already using in my other classes / papers I read. Finally, I don’t have that much pressure by programming languages (PL) people to get sucked into the things they all talk about (types, category theory blah blah blah) in Lean. Those things exist, but there are mathematicians who just use them because they want to do things and be left alone, except if they are stuck and have questions to ask. And that sort of community is fine by me.
• It made me realize that I can completely learn and use these tools (I liked Isabelle as well, but sticking with Lean for now), and I don’t have to be interested in Programming Languages (not everyone wants to build languages! I wish some communities would stop selling formal verification as “PL” because there’s a distinction that can be missed between the communities; I don’t want to build a compiler in a functional programming language and feel superior about it even though no one uses it lol), but just use it as a tool for checking my assumptions about cryptography as I work through a system (modelling behavior, verifying my assumptions are correct). So that’s kind of been my goal. Plus, a lot of Mathematicians seem to like it, so unlike some of the other tools, it’s not a tool that would distance me from the community I want to be a part of as I continue to do research (i.e. Mathematics and post-quantum cryptography).
• PL is its own rabbit hole, and I don’t know if it’s just the culture but I don’t want to feel inferior because I don’t use some random unicode in Vim or Emacs or something from some random library for something I honestly don’t need because I don’t want to make a language or do some compiler thing; I just want to be able to prove thing on a piece of paper, and check it in a programme. So I really liked that this workshop had a breadth of tools, but then problems to solve using a theorem prover of your choice.
• What was interesting is that people at the workshop thought I was more “Mathy” on the scale of people there, which was interesting. And they were asking me about how to get into more “Math things”. So that was surprising, because in the past when I was hanging around PL people, they’d wave their knowledge of compiler stuff as being because they were more Mathy, but now that I’ve spent quite a bit of time just hanging out with Mathematicians, maybe I might know some more things now? In any case, maybe those initial PL people I met (not at the workshop) were just kind of insecure jerks? Who knows; I’m just super happy for this experience at this workshop, and for having so many friends who are Mathematicians, which has allowed me the opportunity to see beauty in what they dedicate so much of their time and energy into.
• It was also the first time that I went to a CS workshop and participants admitted that they felt insecure in their knowledge, but that they wanted to get better. I think that that deepened the connection between participants, because they were willing to be vulnerable and to admit that they weren’t experts, and that we were here to learn from each other and to build a community, and that they found this stuff to be challenging.
• Also, finally, good news: I got into another workshop on my topic of research, which will be in August! I’m super stoked about that!

Here are some photos from the summer school!

• On the way to San Francisco via Caltrain!

• On the Stanford Dish Trail!

• At Fisherman’s Wharf in SF!

• Also in SF

• Making our way back to Caltrain at the end of the night

• At the dish at Stanford Dish trail.

• Beautiful sunset at Stanford Dish trail.

• Touring Stanford

• Union Square in SF photo

• Someone asked Lamport a GPT generated question during the Q&A session

• Learning TPTP from Geoff

• Wine made by scientists at SRI!

• Carolyn talks about “A basis for a Mathematical Theory of Computation”. Coincidentally, the first Meetup I ever attended in LA was on a paper by Hoare which cites this paper. It was my introduction to Computer Science (and the very next day I went to a Haskell meetup).

• Andrei gives out certificates from the summer school with Shankar. Andrei is the creator of EasyChair, but also is heavily involved in the Vampire Theorem prover, along with Laura, who was an exceptional lecturer, and basically taught us how to build a theorem prover from the ground up and how Vampire is optimized. Everyone raved about her lectures!

• Banquet desserts

• Jesse gives a talk on Verifying LLMs and Challenges in that space that could benefit from a formal methods approach.

• elote! I’ve been dreaming about elote since there isn’t good elote where I live!

• On our hike at Stanford Dish Trail

• At Stanford at the Denning House for a photo op.

In Conclusion

• I highly recommend it!
• There are a number of fields that could benefit from these methods, and in particular, what they emphasize is in particular fields that do not know they necessarily need them, rather than just the typical “programming languages” approach. In fact, I used to think that PL was formal verification, but they’re two quite separate fields, and I really enjoyed learning about them in a context that wasn’t just focused on programming languages techniques and approaches.
• For Formal verification, you don’t need to build a compiler; you can think of anything from verifying a process of logic for something like an autonomous car or a washing machine. Basically, anything where you might want to model the process of thinking and how things might go wrong and mitigate those risks. I think that’s a much better sell than the muddied belief that you need to write a compiler for things or a programming language. So this opens up the possibilities to a lot of fields where you have general problems of uncertainty or critical systems. And that’s kind of how they had us think about things, which I appreciated. As they said in a recent MSRI anniversary panel, “Mathematics is clarity of thinking”. And bear in mind, PL is not “mathematics”; it is an applied discipline (at least in my mind for now) of compilers / theory of computation + from Model Theory, which is the discipline of Logic in Mathematics. There are many areas of Mathematics that are beautiful and people should take the time to be exposed to more of them, in the same way that people should not just assume that “Machine Learning is Mathy” means if you learned ML you’d be exposed to all the Maths.
• A final misconception I hear from people in PL is that “Machine Learning people can’t do Mathematics”. I think that that’s a wrong assumption, in the same way that (forward-backward and backward-forward proof lol) we can’t assume all PL people are experts in Mathematics (also wrong; if you’re doing mostly implementation stuff, that may not necessarily be the case). It depends on one’s discipline, and there is a range within people work depending on their specialization. For example, someone like Jesse works in ML but has a background in Formal Verification (his advisor worked on the Kepler Conjecture) and has a PhD in Mathematics, and has given talks and run workshops on topics Pure Mathematicians care about (like Langlands and Sheaf Cohomology), so he actually has a stronger background than many PL people. But that is not necessarily the case for all PL people. I guess that even writing this out logically shows that some people who do applied logic for their work haven’t thought deeply of all the cases.
• I think it would be better to work together and to respect the boundaries of disciplines; all of this work takes effort and years of gaining expertise. Saying that because someone processes data that “that’s easy” is silly. We all have things we are good at or are willing to spend lots of time on, and other things we don’t enjoy, and we all need progress from all disciplines. I don’t think it serves the PL community to be constantly bashing ML, or vice versa. If it turns out that they need systems of data verified, and programmes to do that, then we all benefit. But creating rifts between those communities and teaching the new crop of researchers superiority complexes doesn’t help anyone. Plus, if fields like applied ML do need more guardrails in their systems, we should be open to having these conversations with them in a way that isn’t offputting, and to help them see the value of working side by side with communities like that of Formal Verification.
• Someone (in PL) literally walked up to someone in ML once (first year grad student) and said “that’s not a lot of Math isn’t it?”. Like wtf what is the point of that except if your intent is to make someone feel bad?
• I find those kinds of things (“What you do (in terms of research) isn’t hard”) to be very toxic as someone who is an early-career researcher. If someone recognizes the value a community might provide to a problem in another field, it helps everyone.
• I was really inspired (and I always am when I visit Silicon Valley specifically, or places like JPL or CHM) by the depth of knowledge of the mentors for our workshop: Shankar, Laura, Tim, Pamela, Geoff, Andrei, and their humility. I remember that at one time, someone asked a question to Carolyn about the future of the field, and what we could learn from, and Pat Lincoln made the case that Carolyn’s own work has been not appreciated as much, and Shankar explained over lunch one time how much of a genius she was. Having understood the effects of things like bias / homophily in the academic community, I am thankful that her own colleagues acknowledged how much of a great mentor she has been to them, and to her genius. So we all left wanting to read and to know her work. I left with so many interesting papers to read, and with so many thoughts.
• Shankar had a great chat with us during one lunch session about why the field needs people of all disciplines and less of the bro-y culture in tech and science. I have so much respect for him; he is one of the most knowledgeable guys, with a solid mathematical background (apparently I was the only person in the room who knew about the Pigeonhole principle for one of the sessions, which he spoke about quite a bit; I only learned it because of my Combinatorics professor!) and with a deep love for mentoring others. I learned so much from him and I left with a deep respect for him and others at SRI. And I loved that there was a consistent thread of thinking before programming, writing things down, as opposed to rushing to programme things.
• When people think about Silicon Valley, meeting these kinds of people comes to my mind; these are the parts I want to remember in lieu of the empty, shallow or dark parts. Research institutions where people share ideas and dream about a future for everyone in these labs like SRI, in the pursuit of of an ideal of science that doesn’t just make the lives of the elite better. Their passion for mentoring, for understanding technology in a way that benefits humans, their empathy and deep knowledge has enriched my time in a way that will stay with me for the rest of my life. Being chosen to participate at this workshop enriched my experience in grad school, was humbling, and I felt really valued here, and I’m really grateful for the experience. I never doubted during my time here that I too, could be a scientist one day, here.
• Anyways, I learned so much, and it was very applicable to my area of research! I would definitely like to return within a year, having stuck with Lean and with the working group (using PVS) to see how that would impact my experience.

That’s it