3 ms·
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
by jandrese 10mo ago
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."
- TimTheTinker 10mo agoMost 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.