Microsoft Research: intent formalization is the grand challenge
Shuvendu Lahiri argues that turning informal intent into checkable specifications will decide whether AI makes software more reliable or just more abundant.
In a paper titled Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents, Shuvendu Lahiri of Microsoft Research names the gap between what a user means and what a program does: the intent gap. AI-generated code, he argues, widens it. His answer is intent formalization: translating informal intent into formal specifications that can be checked, at whatever level of rigor a project needs, from lightweight tests to full proofs.
Why it matters for structured intent: this is the strongest research statement yet that intent, not code, is where reliability will be won or lost. Structured intent shares the goal and adds priorities, origins, and one intent carried into several implementations.