Posts

by Shriram Krishnamurthi

When Anthropic published a report this week on how AI is making formal software verification practical at scale, it contained an experiment with deep Brown CS roots. Anthropic asked Claude to write an interpreter for a large chunk of Python, in Rust, and then to prove that it follows the CPython semantics “outlined in an academic paper”. That paper is Python: The Full Monty: A Tested Semantics for the Python Programming Language, published at OOPSLA 2013, and much of it was built by undergraduates.

Why does this paper matter? Because you can’t prove a program correct without saying what “correct” means. For Python, the language is defined by prose, an implementation, and tests, none of which is a formal semantics. The Full Monty paper boiled Python down to a small core language, λπ, gave a precise translation from real Python into that core, and tested the combination against CPython itself. That gave Claude the specification it needed, and Anthropic built on that.

The paper’s origins are as unusual as its afterlife. In fall 2012, when MOOCs were the shiny new thing, Brown’s programming languages course, (then) CS 173, opened its doors online to learn about the format first-hand. Among its assignments, students wrestled with real, messy Python: they wrote an interpreter for a small core, translated the language down to it, and checked their work against Python’s own test suites.

When the semester ended, a handful of students were invited to push all the way to (nearly) full Python. The effort was led by Joe Gibbs Politz, then a Brown CS PhD student, who had led the MOOC. Three of the team were Brown undergraduates: Sumner Warren, Daniel Patterson, and Mae Milano. Three came from far beyond College Hill: Junsong Li was an undergraduate in China who later came to Brown as a master’s student; Anand Chitipothu was a professional programmer in India; and Alejandro Martinez, from Argentina, was an IT professional and triathlete.

Noticing the amount of labor this project (and other similar formalizations by the group) had taken, the programming languages group decided to try using machine learning to tackle this problem. Their blog post from 2013 concluded with, “[W]e have decided to try to use machine learning instead. Once again, machines may put people out of work.” At the time it was intended to be sardonic; now it may be real, but in a good way! Having machines do this work frees up humans to do much more cognitively interesting work. But in the meanwhile, the machines are directly benefiting from the work that those 1730 students did, and everyone benefits from the result.

Brown CS has no financial involvement in any of the people or organizations mentioned above and has not been compensated in any way for this story. The views and opinions expressed above are those of individuals, and do not necessarily state or reflect those of Brown CS, nor does their publication here constitute an endorsement of them.