3 ms·
> not enforced in the case of ZZ I don't think it's really even possible for a language to force the programmer to give a proper formal specification. We may
by MaxBarraclough 7y ago
> not enforced in the case of ZZ
I don't think it's really even possible for a language to force the programmer to give a proper formal specification.
We may want the formal spec to grant some leeway, i.e. not to specify the exact output/behaviour, but instead to express certain important constraints. For instance, we may not care which traffic-light turns green first, so long as the system preserves the important properties about safety and liveness.
If we wish to support such flexibility, we can't stop the programmer from expressing all output states are valid.
If we don't wish to support such flexibility, what we're really doing is comparing against a reference implementation.
- zozbot234 7y ago> I don't think it's really even possible for a language to force the programmer to give a proper formal specification. The language, probably not. The standard library can certainly require detailed-enough formal preconditions to make its code defect-free, meaning that any remaining bugs can then be directly traced to the programmer's code.
- MaxBarraclough 7y agoYou mean that, for instance, a standard-library generic sort function, might require that your comparator function behave correctly when the arguments are reversed? That's an interesting idea. Like Java interfaces, but with formal contracts. I doubt that putting these contracts into the standard-library would give you good proof-coverage though.