Sealed Rust Update | Hacker News Reader

Sealed Rust Update

ferrous-systems.com

163 pointscsomar32 comments

I am surprised they didn't mention Iris[1] and RustBelt[2] projects. Iris works on creating the formalization framework based on separation logic and Coq. They have the Rust code model specifically[3].

[1] https://iris-project.org/

[2] https://plv.mpi-sws.org/rustbelt/

[3] https://gitlab.mpi-sws.org/iris/lambda-rust

This is mainly a lapse. Thanks for highlighting them, they do awesome work!

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.

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.

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.

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.)

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%...), 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.

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.

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.

> 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.

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.

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.

The working URL https://ferrous-systems.com/blog/sealed-rust-the-plan/

I don't get why there is so much love for Rust but so little love for Ada?

Did Ada - or rather its proponents - make any effort to get people to learn it? If I google for "Ada programming language" I do not even find what could be an official site? I thought it could be adacore.com, but that's a commercial offering. Wiki tells me it could also be adaic.org, which errors out with "SSL_ERROR_UNSUPPORTED_VERSION" in current Firefox. Even if I could access the site: Would I find tutorials? Other supporting material? Explanations why I should use Ada?

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).

Agreed, Ada's documentation is sparse and hard to find. Unfortunately, the best resource I've found for learning it from the ground up is the textbook "Programming in Ada 2012" by John Barnes. It's a bit pricey, but the core of the language hasn't really changed since Ada 95, so a used copy of an old edition will get you started.

AdaCore's got some decent learn-by-example stuff here, but it doesn't cover every aspect of the language. https://learn.adacore.com/courses/intro-to-ada/index.html

Wikibooks has a pretty comprehensive book on Ada Programming, but there are still a lot of missing pages. https://en.wikibooks.org/wiki/Ada_Programming

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. http://www.ada-auth.org/standards/ada12.html

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.

There's a lot of love for Ada. Unlike Rust, Ada is already an approved language and toolchain for safety-critical software development. That Sealed Rust is trying to do what it takes to get Rust into the approved language & toolchain category along side Ada is entirely the point, and what makes it interesting.

I guess, due to a couple of things.

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.

https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-auto...

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.

Potentially interestingly, it looks like there's ongoing work to get Ada compiling to wasm via LLVM too.

Hello World style demo:

https://blog.adacore.com/use-of-gnat-llvm-to-translate-ada-a...

Getting started with Ada is hard. The best compilers and runtime for it are commercial, and especially getting it to work in embedded (where it really shines) is not at all straightforward. I've looked at it a few times and never really been able to get anywhere useful with it, and came away with the impression the best way is to drop a few thousand on it or work on a government contract.

There's plenty of love for Ada, more than ever.

https://blog.adacore.com/the-emergence-of-a-new-ada-era

From my perspective, I'd say it's because there isn't much talk about Ada as a technology. It comes up a lot when Rust is discussed, but I never see details besides built-in ranges for numbers. I can't even remember ever hearing anything much about the library/tooling Ada ecosystem.

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.

There's still tons of love for Ada at all the places where we spoke to.

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.

Ada is not cool. More seriously, GNAT crashed all the time in random ways when I tried it, and when I tried adacore on stm32, the timing functions were based on systick, that’s a non-starter for me, and I didn’t want to start learning a new system by re-implementing part of its internals.

Ada get plenty of love where it matters : actual industrial usage in critical systems.

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.

As someone who lead a lot of the talks hinted at in the blog post: it translates to 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 also see your devaluing of effective use of marketing and some peoples background on the internet.

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.

You seem to be implying that the horrible state of IoT is not mostly the fault of the web integration layer.

I want much more runtime performance out of rust more than anything else. Faster builds are second on the list. This probably doesn't even make top 10. Who is this aimed at? And I would hate for those top goals to be subverted for this.

From the previous blog post ("Part 1: The Pitch"[1]):

> 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)

[1]: https://ferrous-systems.com/blog/sealed-rust-the-pitch/

I work in medical devices and out-of-the-box rust would be a much better option than the C++ systems we build!

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)!

Different people have different needs. There’s also room for many different people to work on different problems at the same time without imposing constraints on each other.

1.) Do you work in safety critical software? If not, this is not for you.

2.) This is a third party, this is not taking resources from generic rust.

Reply on news.ycombinator.com