Trust the Spec, Not the Code - A Specification-First, AI-Assisted Case Study in Online Banking
It is argued that AI removes much of that cost: natural language enriched with lightweight mathematics, written in \LaTeX, can serve as an intermediate specification language that is precise enough to reason over and prove, while a large language model reviews it for ambiguity, drafts proofs, and generates the implemen...