4 ms·

Can you articulate what a spec for a programming language entails in your mind. I am sure it is a niche opinion/position, but I base any discussions of formal s

Can you articulate what a spec for a programming language entails in your mind. I am sure it is a niche opinion/position, but I base any discussions of formal specification of a language on ‘The Definition of ML’. With that as a starting point I don’t see how the implementation process of a compiler would do anything that could force a change to the spec. Once the formal syntax is defined, the static and dynamic semantics of the language laid out and those semantics proved approximately consistent and possessing ‘type safety’ (for some established meaning of the words). Any divergence or disagreement is a failing of the implementation. I’m genuinely interested in what you expect a specification of Rust to be if, as your comment suggests, you have a different point of view?

estebank 3y ago
A specification can be prescriptive (stating how things should work) or descriptive (stating the observable behavior of a specific version of software). For example earlier in Rust's post-1.0 life the borrow checker changed behavior a few times, some to fix soundness bugs, some to enable more correct code to work (NLL). An earlier spec would have described different behavior to what Rust is today (but of course, the spec can be updated over time as well). How should the Rust Specification represent the type inference algorithm that rustc uses? Is an implementation that can figure out types in more cases than described by the specification conformant? This is the "split ecosystem concern" some have with the introduction of multiple front ends: code that works on gccrs but not rustc. There's no evidence that this will be a problem in practice, everyone involved seems to be aligned on that being a bad idea. > Any divergence or disagreement is a failing of the implementation. Specs can have bugs too, not just software.
- throwaway17_17 3y ago
  I think it was probably a rhetorical question, but with regards to type checking, as with ML, type inference is an elaboration step in the compiler that produces the correct syntax of the formal language defined in the language definition. Specifying the actual implemented algorithm that translates from concrete syntax to abstract syntax (and the accompanying elaboration to explicit type annotations) is a separate component of the specification document that does not exert any control or guidance to the definition of the formal language of the ‘language’ in question. I think this may be a large point of divergence with regard to my understanding and position on language specifications. I assume when posts have said Rust is getting a spec, that that included a formal, ‘mathematically’ proven language definition of the core language. I am aware that is not what C or C++ or JS includes in a spec (and I don’t know if that is true for Ada), but I was operating under the assumption the Rust’s inspiration from Ocaml and limited functional-esque stylings that the language would follow the more formalized definition style I am used to.
  - estebank 3y ago
    Look at Goals and Scope in https://blog.rust-lang.org/inside-rust/2023/11/15/spec-vision.html https://blog.rust-lang.org/inside-rust/2023/11/15/spec-visio... for what the Rust spec will be.

estebank 3y ago

A specification can be prescriptive (stating how things should work) or descriptive (stating the observable behavior of a specific version of software). For example earlier in Rust's post-1.0 life the borrow checker changed behavior a few times, some to fix soundness bugs, some to enable more correct code to work (NLL). An earlier spec would have described different behavior to what Rust is today (but of course, the spec can be updated over time as well). How should the Rust Specification represent the type inference algorithm that rustc uses? Is an implementation that can figure out types in more cases than described by the specification conformant? This is the "split ecosystem concern" some have with the introduction of multiple front ends: code that works on gccrs but not rustc. There's no evidence that this will be a problem in practice, everyone involved seems to be aligned on that being a bad idea. > Any divergence or disagreement is a failing of the implementation. Specs can have bugs too, not just software.

throwaway17_17 3y ago
I think it was probably a rhetorical question, but with regards to type checking, as with ML, type inference is an elaboration step in the compiler that produces the correct syntax of the formal language defined in the language definition. Specifying the actual implemented algorithm that translates from concrete syntax to abstract syntax (and the accompanying elaboration to explicit type annotations) is a separate component of the specification document that does not exert any control or guidance to the definition of the formal language of the ‘language’ in question. I think this may be a large point of divergence with regard to my understanding and position on language specifications. I assume when posts have said Rust is getting a spec, that that included a formal, ‘mathematically’ proven language definition of the core language. I am aware that is not what C or C++ or JS includes in a spec (and I don’t know if that is true for Ada), but I was operating under the assumption the Rust’s inspiration from Ocaml and limited functional-esque stylings that the language would follow the more formalized definition style I am used to.
- estebank 3y ago
  Look at Goals and Scope in https://blog.rust-lang.org/inside-rust/2023/11/15/spec-vision.html https://blog.rust-lang.org/inside-rust/2023/11/15/spec-visio... for what the Rust spec will be.