They are also not quite what Sealed Rust is about. RustBelt is about formally verifying Rust and improving the understanding of the language.
Sealed Rust is mainly about the industrial adoption process. It's not meant as a replacement or competing project, quite the contrary: RustBelt existing is a huge motivator and a major stepping stone to build on.
We are also personally in touch through the Rust project.
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.
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.
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%...), 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.
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.
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.
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.
Those industries you mention are not niche.
If you want people to use your language you have a to put in work. Even more for a language with the reputation of Ada (the sibling comment by pjmlp gives a good overview).
AdaCore's got some decent learn-by-example stuff here, but it doesn't cover every aspect of the language.
Wikibooks has a pretty comprehensive book on Ada Programming, but there are still a lot of missing pages.
Finally, the language reference covers everything, but it's formatted in the most unusable and difficult to search way I've ever seen. The source files for the reference are maintained by a single editor who invented his own markup language and parser for converting that into HTML and PDF. That may have been acceptable in 1995, but it provides a significant barrier to adoption today. I've made a few attempts at coercing these sources into docbook, but so far I've found I'm not clever enough to untangle this mess.
So yeah, just buy the textbook... Skip the first few chapters, they're basically just advertising that tells you how great the thing you're about to learn is, which I find to be in poor taste.
1 - There is a younger generation that thinks C and C++ are the only game in town, and never learn about myriad of systems programming languages going back to 1961.
2 - This same generation is very averse paying for tooling and among the six surviving Ada compiler vendors, GNAT is the only free one, and even then discussions about its licensing pop up ('cause lets have free beer)
3 - Ada suffers from the whole bondage vs cowboy programming theme that was so common in the early 90's. Where many could not grasp the benefits of type driven programming.
4 - You need a strong engineering background, specially on high integrity computing domain, to understand why Ada offers what it does
6 - Due to high integrity computing domain, Ada tends to be used in domains that many don't find cool, government contracts, train control systems, airplane avionics, pages long contracts with project management very waterfall like even when they pretend to be agile now
7 - It is definitely not a language for the Silicon Valley culture.
However thanks to Ada being there first, having the certified compilers, being deployed into production during the last 40 years, with the increasing number of security exploits, some companies have been adopting Ada, NVidia being one of them.
Two of the reasons, for why Ada and not Rust, was precisely the lack of maturity of Rust on high integrity computing and Ada being more approachable to their engineers. They did a webinar about the adoption process.
Hello World style demo:
Also, Ada users seem to be more focused on technical content about safety/mission critical things, like this discussion. But this is a meta-area where no specific features or solutions are in focus. When there's a discussion about zero-copy parsing, compiler optimizations, platform support, scalability or any other everyday technical topic, noone knowing Ada seems to join in with their perspective and experience.
So my advice to the Ada community would be to talk more details, talk more about what you love. Tech is a big field and it's currently a lot of work to get to know Ada from the outside.
Rust, Swift, Nim, Zig and other languages are the driver of a current resurgence of debates around the embedded toolstack, though, which Rust leading the pack by having the most upfront "we want to talk" messaging.
It is not clear to me how the internet hype surrounding Rust which seems mostly driven by people coming from dynamic languages and former web developers actually translate to use where it counts.
I also see your devaluing of effective use of marketing and some peoples background on the internet. Memes like "InternetOfShit" wouldn't have happened if hardware builders would appreciate the skill sets of web engineers (e.g. running applications that are constantly under automatic attack).
Ada is still on the table though. In most places we spoke to that evaluated Rust as the next language, the other language on the table was Ada.
I fear you are bringing your own prejudice to my post.
I merely pointed that the most vocal supporters of Rust are not people doing safety critical software which is supposedly Rust forte. The whole "InternetOfShit" thing is purely on your own.
> We hope that the Sealed Rust effort would be applicable to any developers working in safety critical software domains, such as:
> Automotive (under safety standard ISO26262)
> Industrial (under safety standard IEC61508)
> Robotics (under a number of safety standards deriving from IEC61508)
> Medical Devices (under safety standard IEC62304)
> Avionics (under safety standard DO-178)
There is competition in this space from qnx as well.
Take a look at the medical device alarms standard IEC 60601-1-8. It's possible to provide a very generic implementation of the standard for high, low and medium priority alarms. Could act as a trojan horse to introduce your back end messaging, logging, shared memory infrastructure - all developed according to ISO 62304 (of course)!
2.) This is a third party, this is not taking resources from generic rust.