4 ms·
I still believe in a future where programming-by-specification and advanced theorem proving systems result in the ability to make systems that are provably with
by TTPrograms 11y ago
I still believe in a future where programming-by-specification and advanced theorem proving systems result in the ability to make systems that are provably without a certain class of bugs. Then it would be possible to upgrade systems effortlessly by simply proving that they satisfy the same primary specifications.
Then of course writing the spec is the hard part, but I'd at least be interested in seeing what those challenges turn out to be like.
- Palomides 11y agois there any difference between a sufficiently rigorous spec and actual programming?
- andrewflnr 11y agoDepends on what you mean by "sufficiently rigorous". There's a sense in which an algorithm description is just a more detailed spec, but if a spec is just "specify all properties of output", that can be described in predicate logic. The spec language doesn't necessarily have to be turing complete (I think).