CS Colloquium: Nikhil Swamy on The ART of Agentic Proof-Oriented Programming: Audits, Rubrics, and Templates

Please join us in ECCR 265 or on Zoom! Abstract: AI-based program synthesis is now widespread. While AI agents churn out large amounts of code from informal natural language descriptions, comprehending this code and assessing its correctness is a major challenge. Having agents code in proof-oriented languages can help, using theorem proving tools to check that the code conforms to a specification, and allowing humans to focus on assessing formal specifications against their informal intent. However, when confronted with reviewing messy agent-generated specifications, one may be no better off than trying to understand the code itself. This talk draws on my team's experience this year using agents to program & prove in F*, a proof-oriented language developed at Microsoft Research. In just a few months, with agents, we have built several verified libraries and systems, ranging from formalizations of algorithms textbooks, to garbage collectors, cryptographic libraries, a variety of Interne...