Specifications Don't Exist
Summary
The article argues that formal specifications are rare and often impractical for most systems, explaining why many specs exist only informally (docs, tests, user stories). It uses the PDF format and the DARPA SafeDocs project as case studies to show how formal verification remains costly and how AI-assisted tooling might make complete proofs or partial specifications more feasible in the future. It suggests focusing on useful, partial specifications like test cases rather than trying to declare a perfect universal spec.