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.

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.

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.

for example check out the err::checked() theory which enforces that a function call must be followed by err::check.

similarly, i expect a community will come up with other standard contracts such as must_not_copy() for secret values that may not be copied.