• 4:41: Reference to Peter Naur’s 1985 paper Programming as Theory Building
• 5:45: With AI, nobody has the theory, so the code is effectively legacy immediately after writing.
• 13:18: But with AI, we can also connect natural language to formal verification
• Demo of LemmaScript with Dafny
• 24:36: Presentation of Djinnlang paper, unambiguous specification with an LLM in the compiler
• 26:53: Mention of Guardians of the Agents, Formal verification of AI workflows
• 32:24: Instead of “code review”, we should review “coherence of the system”

Nada Amin is a professor at Harvard SEAS. A research assistant at SEAS receives between $53k and $83k per year.

score 1 · canonical