alt Hacker NewsThe danger of this is people start asking about formally verified specs, and down that road lies madness.
"If you can formally verify the spec the code can be auto-generated from it."
The danger of this is people start asking about formally verified specs, and down that road lies madness.
"If you can formally verify the spec the code can be auto-generated from it."
Most formal "specs" (the part that defines the system's actual behavior) are just code. So a formally verified (or compiled) spec is really just a different programming language, or something layered on top of existing code. Like TypeScript types are a non-formal but empirical verification layer on top of JavaScript.
The hard part remains: translating from human-communicated requirements to a maintainable spec (formally verified or not) that completely defines the module's behavior.