PoP Seminar - Brian Milnes
May 13, 2026 2:00PM—3:00PM
Location:
In Person and Virtual - ET
-
Traffic21 Classroom, Gates Hillman 6501 and Zoom
Speaker:
BRIAN G. MILNES
https://github.com/briangmilnes/APAS-VERUS
This talk focuses on my experiences using LLM AIs to generate Rust code for Acar and Blelloch's 'Algorithms Parallel and Sequential' textbook. I implemented all of its 121 algorithm variants, 81 of which are parallel, and then verified them in the Verus formal verification system. This work puts to rest the question of: can current AI LLMS be used to prove practical Industrial-grade, performant algorithms.
I'll discuss my experiences, the time, the costs, and the software engineering discipline developed using programmatic techniques to drive down the agentic coding and proof costs. I'll review Rust's strengths and weaknesses, discuss Verus's strengths and weaknesses and review AI agents and their interfaces.
From this work I am able to provide three metrics, which I call the CPR$: - C, a reasonable costs per lines estimate of code in agentic programming a textbook, - P, and a reasonable costs per lines of proof while proving that code and learning Verus.
The bottleneck in agentic programming and proving is now the time to review the code and proofs. I derive an exact measure, R, of how proven code reduces the cost of programmer review.
—
I have done two years of industrial AI programming languages development, followed by seven years of AI research at Carnegie Mellon School of Computer Science (SOAR). Then two years of programming research in programming languages focusing on their use in systems programming and networking (Fox Project).
I was then drafted into the Internet boom and directed groups working in systems, performance, operations and architecture for Lycos, Amazon and Zillow. (M.Sc. Computer Science, University of Washington; B.Sc. Mathematics (Computer Science), Carnegie Mellon )
In Person and Zoom Participation. See announcement.
Passcode: 1TRrEL
For More Information:
yano@cs.cmu.edu