3 ms·
> Go’s spec isn’t formally proven, for example, so you could make a similar claim: how can people know that it all works without a proof? that's moving the goa
by f2f 8y ago
> Go’s spec isn’t formally proven, for example, so you could make a similar claim: how can people know that it all works without a proof?
that's moving the goalposts. let's see Rust's language spec finalized first, then we can talk about it being proven. without the two you shouldn't throw stones.
- skybrian 8y agoI actually think a mathematical-flavored spec where a proof would be meaningful would be a bad idea to the extent that it makes the spec less readable by ordinary users. For example, Dart has a more mathematically flavored spec and it's not readable by most people. Of course, formalisms can still be useful, but as a matter of writing style, maybe it's better to put that sort of thing in an appendix? (As sometimes done for grammars.)
- qznc 8y agoI would rather have a formal spec as the definitive one. Deriving a formal spec from a readable one seems to hit ambiguous cases all the time. Just look at publications that do that for C or Java. With a formal spec you could also derive an implementation automatically which is a great useable reference. Look up the K framework for one possibility.
- electrograv 8y agoOne can generate an informal spec from a formal spec. One can NOT generate a formal spec from an informal spec (or else that “informal” spec would actually be formal, after all). So, a formal spec is strictly better than an informal one — it enables all the benefits of an informal spec, via the ability to generate any number of informal specs from it in many human languages, cultures, levels of detail, etc., and of course enables things like compiler reproducibility (which you cannot do at all without a formal spec). That being said, any spec is probably better than no spec.
- skybrian 8y agoSince many programmers are not mathematicians, a formal spec will always have a smaller audience than a well-written spec written in English. You cannot automatically derive good writing from pure mathematics. As a result, neither is strictly better than the other. They have different audiences and serve different purposes. The audience for pure mathematics is quite small.
- burntsushi 8y agoThere are no stones being thrown and no goalposts moving. Go's specification is clearly in a much more advanced and useful state than Rust's. The point is to respond to "how can people know." That is, it is a measure of degree, not binary.
- steveklabnik 8y agoYes, this is exactly it, thank you.