Title: Correct-by-Construction Programming in the Era of Generative AI

Speaker: Nada Amin,  Assistant Professor of Computer Science at Harvard SEAS

Abstract: Generative AI systems can now produce and modify software at unprecedented scale, but assurance has not kept pace. As code is increasingly generated, repaired, and evolved automatically, traditional approaches to correctness (manual review, testing, or post-hoc verification) become brittle and difficult to sustain.

This talk argues for correct-by-construction programming as a unifying response to this shift. Rather than treating verification primarily as a check on completed programs, I advocate for programming language foundations that make correctness a structural property of how software is built, transformed, and extended. I will trace this idea across my research, from multi-stage programming that turns interpreters into compilers, through extensible semantics that allow languages and proofs to evolve without invalidating prior guarantees, to recent verifier-in-the-loop systems that integrate large language models as heuristic generators under formal control.

Speaker Bio: Nada Amin is an Assistant Professor of Computer Science at Harvard SEAS. Her research combines programming languages and artificial intelligence to create systems that are correct by construction.

Before Harvard, she was a University Lecturer at Cambridge, part of the team behind the Scala programming language at EPFL (where she completed her PhD), and a software engineer at Google working on the compiler infrastructure supporting Gmail and other Google Apps. She holds BS and MEng degrees from MIT.

There will be refreshments before the colloquium at 2:15pm outside of LL2.224