4 ms·

This is an important effort, but it's weird (disconcerting?) to me that something so fundamental as a formal language specification (for a language that adverti

by _bxg1 7y ago

This is an important effort, but it's weird (disconcerting?) to me that something so fundamental as a formal language specification (for a language that advertises safety as a key feature) is being bootstrapped not by the core team, but by a third party. It doesn't feel like that's something you only need "collaboration with" the core team about. I can't think of anything that's more "core". The rest of it makes sense as an auxiliary effort: working directly with relatively niche industries on certification, narrowing down a fully-safe subset of the language, etc. But I don't see how Rust can ever come into its own in the space that it's targeting without having a real specification outside of the compiler.

chrismorgan 7y ago
Speaking bluntly: Almost everyone using the language at present is getting by just fine without this. As a normal Rust developer, I don’t particularly care about a formal language specification existing. It’s a long way down my list of nice-to-haves—yeah, it would be nice to have, but there are quite a few other things that would be more nice to have. The core team are compiler and language developers. I’d much rather have them working on the language, rather than a formalisation of the language that isn’t going to benefit me particularly for many years. If there are other people that are interested in doing that work, good on ’em; it’ll be interesting to see what happens, but I don’t want the core developers distracted with this sort of speculative work—for this is a heavily experimental area. This is absolutely a place for only a collaboration, rather than having it being managed by the core team. If the core team were focusing on this, everything would collapse in a heap. The core team is a very finite resource that does not specialise in this sort of thing in any way.
- saurik 7y ago
  I think the argument is that if you said that about C++ everyone would be "yeah: this is just a useful tool, so why do I care?"... but Rust is about safety, and if you don't have a formal model of the language by what reasoning could you possibly have to know it is safe? (And, in fact, every now and then--much less often these days, but still--someone finds a soundness issue in Rust itself, something you would hope to have been able to disprove at the outset using a proof over a formal model.)
  - mikekchar 7y ago
    I know that "Rust is about safety" is the message that gets out, but I don't think it really is. At least, not any more than "Haskell is about safety". Rust is really about zero cost abstractions, IMHO. The borrow checker is a tool that allows you to work towards memory safety with zero cost abstractions. As a Rust developer, I'm actually much less worried about safety than I am about the zero cost. Rust allows me to achieve that zero cost without blowing up in complexity (which is sometimes hard to believe when you are wrestling with a borrow checker problem ;-) ). Having said that, I'm totally happy if there can be formal verification of these things. However, I certainly don't consider it to be job 1.
  - chrismorgan 7y ago
    I care about Rust’s safety. It’s what let me confidently use Rust instead of Python or JavaScript, where I had never felt comfortable with C or C++. But the safety that Rust has already is good enough for me. I know that soundness holes exist (c.f. https://github.com/rust-lang/rust/labels/I-unsound%20%F0%9F%92%A5 https://github.com/rust-lang/rust/labels/I-unsound%20%F0%9F%...), but they are very few, and if they’re realistic (most of those are possible but difficult to trigger and very unlikely to be encountered by real code) they get knocked down very quickly. Frankly I think you’re overhyping the benefits of a formal model (in practice I believe it’s normally only certain subsets of popular compilers that are ever formally verified), underestimating the pernicious presence of bugs even with formal verification, and overvaluing the significance of the remaining 0.00000001% of safety to a working programmer. In line with what mikekchar says, I care about performance and such things more than I care about formal verification of Rust’s safety. I’m happy to hear about this stuff, but I don’t expect it to personally affect me, for the better or for the worse.
  - _bxg1 7y ago
    Not only that, it's much harder/impossible to implement an alternate compiler without a spec to go off of. C++ has multiple compilers which really benefits the ecosystem in various ways; until we have a spec, there's just rustc.
Argorak 7y ago
> This is an important effort, but it's weird (disconcerting?) to me that something so fundamental as a formal language specification (for a language that advertises safety as a key feature) is being bootstrapped not by the core team, but by a third party. It doesn't feel like that's something you only need "collaboration with" the core team about. I can't think of anything that's more "core". This may be a misunderstanding about what Rust core does: it's a project steering committee. The specification work would have to be done by lang and compiler. The Rust language specification is notoriously informal, as many of the current investors in Rust don't care _that strongly_ about it, at least not in the rigorous sense that certification needs. Major features are built by those investors. Sealed Rust is an initiative to collect the stakeholders in having a proper specification happening. Rust has always evolved on stakeholder needs, with those stakeholders providing the work either through staffing engineers or by funding engineers on the relevant teams and often relies on outside engineering/contribution. This is not _as_ different. So, see it this way: we want Safety Critical Rust to happen. For that, we need some form of specification. We're willing to get a specification funded and contributed in a way that is useful to the project and doesn't tie it down.
- _bxg1 7y ago
  The Web isn't especially "safety-critical", and it rapidly evolves to meet stakeholder needs, but it still has a formal specification at the top that serves as the entry point for new features. This single source of truth is the touchstone for all involved parties, is where things get proposed and debated and decided, and then that filters down to browser vendors who implement the spec. This allows vendors to ensure cross-compatibility and allows the languages to be more than just a compiler or interpreter. Having a formal spec isn't specific to the niche industries talked about in Sealed Rust; it's simply good practice for any open language project.
  - Argorak 7y ago
    The web is also well-known for implementation before specification and often specifying vendor-specific extensions because of widespread adoption. A specification is a touchstone, yes, but also a substantial effort. The Rust language is also built with vastly less manpower than the web specification! It's okay that you consider a specification good practice, but there's a ton of open source project that are not specified with the rigor you ask for, which kind of takes away the point... Those industries you mention are not niche.

by _bxg1 7y ago

chrismorgan 7y ago

Speaking bluntly: Almost everyone using the language at present is getting by just fine without this. As a normal Rust developer, I don’t particularly care about a formal language specification existing. It’s a long way down my list of nice-to-haves—yeah, it would be nice to have, but there are quite a few other things that would be more nice to have. The core team are compiler and language developers. I’d much rather have them working on the language, rather than a formalisation of the language that isn’t going to benefit me particularly for many years. If there are other people that are interested in doing that work, good on ’em; it’ll be interesting to see what happens, but I don’t want the core developers distracted with this sort of speculative work—for this is a heavily experimental area. This is absolutely a place for only a collaboration, rather than having it being managed by the core team. If the core team were focusing on this, everything would collapse in a heap. The core team is a very finite resource that does not specialise in this sort of thing in any way.

saurik 7y ago
I think the argument is that if you said that about C++ everyone would be "yeah: this is just a useful tool, so why do I care?"... but Rust is about safety, and if you don't have a formal model of the language by what reasoning could you possibly have to know it is safe? (And, in fact, every now and then--much less often these days, but still--someone finds a soundness issue in Rust itself, something you would hope to have been able to disprove at the outset using a proof over a formal model.)
- mikekchar 7y ago
  I know that "Rust is about safety" is the message that gets out, but I don't think it really is. At least, not any more than "Haskell is about safety". Rust is really about zero cost abstractions, IMHO. The borrow checker is a tool that allows you to work towards memory safety with zero cost abstractions. As a Rust developer, I'm actually much less worried about safety than I am about the zero cost. Rust allows me to achieve that zero cost without blowing up in complexity (which is sometimes hard to believe when you are wrestling with a borrow checker problem ;-) ). Having said that, I'm totally happy if there can be formal verification of these things. However, I certainly don't consider it to be job 1.
- chrismorgan 7y ago
  I care about Rust’s safety. It’s what let me confidently use Rust instead of Python or JavaScript, where I had never felt comfortable with C or C++. But the safety that Rust has already is good enough for me. I know that soundness holes exist (c.f. https://github.com/rust-lang/rust/labels/I-unsound%20%F0%9F%92%A5 https://github.com/rust-lang/rust/labels/I-unsound%20%F0%9F%...), but they are very few, and if they’re realistic (most of those are possible but difficult to trigger and very unlikely to be encountered by real code) they get knocked down very quickly. Frankly I think you’re overhyping the benefits of a formal model (in practice I believe it’s normally only certain subsets of popular compilers that are ever formally verified), underestimating the pernicious presence of bugs even with formal verification, and overvaluing the significance of the remaining 0.00000001% of safety to a working programmer. In line with what mikekchar says, I care about performance and such things more than I care about formal verification of Rust’s safety. I’m happy to hear about this stuff, but I don’t expect it to personally affect me, for the better or for the worse.
- _bxg1 7y ago
  Not only that, it's much harder/impossible to implement an alternate compiler without a spec to go off of. C++ has multiple compilers which really benefits the ecosystem in various ways; until we have a spec, there's just rustc.

Argorak 7y ago

> This is an important effort, but it's weird (disconcerting?) to me that something so fundamental as a formal language specification (for a language that advertises safety as a key feature) is being bootstrapped not by the core team, but by a third party. It doesn't feel like that's something you only need "collaboration with" the core team about. I can't think of anything that's more "core". This may be a misunderstanding about what Rust core does: it's a project steering committee. The specification work would have to be done by lang and compiler. The Rust language specification is notoriously informal, as many of the current investors in Rust don't care _that strongly_ about it, at least not in the rigorous sense that certification needs. Major features are built by those investors. Sealed Rust is an initiative to collect the stakeholders in having a proper specification happening. Rust has always evolved on stakeholder needs, with those stakeholders providing the work either through staffing engineers or by funding engineers on the relevant teams and often relies on outside engineering/contribution. This is not _as_ different. So, see it this way: we want Safety Critical Rust to happen. For that, we need some form of specification. We're willing to get a specification funded and contributed in a way that is useful to the project and doesn't tie it down.

_bxg1 7y ago
The Web isn't especially "safety-critical", and it rapidly evolves to meet stakeholder needs, but it still has a formal specification at the top that serves as the entry point for new features. This single source of truth is the touchstone for all involved parties, is where things get proposed and debated and decided, and then that filters down to browser vendors who implement the spec. This allows vendors to ensure cross-compatibility and allows the languages to be more than just a compiler or interpreter. Having a formal spec isn't specific to the niche industries talked about in Sealed Rust; it's simply good practice for any open language project.
- Argorak 7y ago
  The web is also well-known for implementation before specification and often specifying vendor-specific extensions because of widespread adoption. A specification is a touchstone, yes, but also a substantial effort. The Rust language is also built with vastly less manpower than the web specification! It's okay that you consider a specification good practice, but there's a ton of open source project that are not specified with the rigor you ask for, which kind of takes away the point... Those industries you mention are not niche.