Is there a plan to get a formal Rust language specification at some point?

Hi.

Apologies if this isn’t the right forum/channel.

TL; DR: I understand that there isn’t a formal Rust language specification (akin to C and C++ anyway). Is there a plan to get a formal specification at some point ?

Detail:

I have an OS development background and I work at Arm at Cambridge, UK, in a group where the charter is to promote the use of Arm IP in safety critical domains using open source software as a medium.

We have an internal special interest group where Rust afficionados get together and reason about possibilities with Rust and Arm. It’s fun!

Recently, I informally introduced Rust to some of our long bearded and dyed in the wool C/C++ compiler architects. I noticed a pattern in their responses/opinions which I’ve seen in other similar discussions I’ve had and I’d like to share some points here to get opinions.

The first phase of the discussion is always about convincing ‘them’ about the safety properties. That’s usually not hard with such folk who understand the problem space well.

The second phase which inevitably follows - especially if the person has some experience with safety critical domains (although just productisation exposure is enough) - trends to a point where they ask for a pointer to the formal language specification.

That’s where the conversation usually ends, unfortunately.

Folks who are in the business of assessing and qualifying software and tools for deployment in safety critical areas are usually the ones who simply won’t consider the technical merit alone - they want to see a formal language spec.

I made some good headway with the compiler architects in terms of convincing them of things like the compile time safety guarantees thanks to the ownership semantics, the ability to specify the desired consistency of the memory model for atomics, the elegance of having access to closures, iterators, generators in a systems programming language, the super FFI possibilities, the whole shebang. Everyone raves at those bits. The conversation always ends up talking about evidence of misc ecosystem uptake and it always ends at the language specification point.

I don’t think this is subject to the safety critical domain alone BTW. I recently co-presented about Rust and Redox OS at a conference in Vancouver where 2 reps from Arm silicon partners came up to us later and said pretty much exactly this: We like Rust and we want to use it in our general product roadmaps (mobile and enterprise were spoken of). But we see that as being too risky unless the language specification is in place and there is evidence of both compliance to that specification in the Rust tooling vendor-o-spheres as well as evidence of emerging production deployments.

So: I’ve been given to understand that a formal language specification doesn’t exist. The best articulation of a specification is embedded in the Rust compiler sources.

Is there a plan to get a formal language specification - akin to C/C++ - at some point ?

I don’t think it’s important to have it right away. It’s more important to have a practical vision towards when and how such a specification might come about. That in itself will help allay fears and trend well in such domains over time.

Thoughts ?

Thanks for hearing me out!

26 Likes

I believe there’s a lot of interest in a formal spec, but as is, it doesn’t look like the work needed to write one is productive for the people in the position to do so. As you mentioned, the compiler is itself a formal spec for the behavior of the language, and that’s the spec the experts need to understand to work with the language in any practical sense. That being said, there are things being worked on wrt unsafe code guidelines and deeper language features that would undoubtedly need to be included in a formal spec which aren’t fully worked out yet.

I believe a big part of the motivation for specifying C/C++ standards was to ensure compatibility between different compiler implementations. Naturally if there’s only one compiler implementation – or no plans for another – the motivation must be different.

2 Likes

Yes, there is. In fact, the EU has even put in a ton of money towards such a thing: http://plv.mpi-sws.org/rustbelt/

It’s a huge task, but there’s multiple efforts, including that one. Just like it took C and C++ on the order of decades, it’s gonna take us a while too.

9 Likes

Hi.

Hmm. Perhaps we are talking at cross-purposes here ? When I say formal language specification I don’t mean formally verifying the language for implementation correctness.

I mean something akin to https://isocpp.org/std/the-standard

Or have I misunderstood ?

Thanks

1 Like

They’re intertwined; we don’t want to create a spec that ends up being impossible to have formal semantics for.

If you want an informal spec, the reference isn’t complete, but is the closest thing we currently have.

4 Likes

Well, they’re intertwined for sure. But should they be lock-step dependent ?

A formal language specification is - from my layperson’s PoV (and I can easily get some expert opinion to be sure) - orders of magnitude easier to articulate than a formal proof of implementation correctness of the language itself.

Can you please cite some sources where I can educate myself further ? I assume the RustBelt link you pointed to sheds more light on this subject matter - specifically the aim to keep the language specification and the formal verification in some sort of coupling ? Thanks.

Overall - what I’m learning - and meaning to relay here - from professional exposure to the safety critical ecosystem, from the PoV of a processor IP silicon designer is that unless there is a practical path to a language specification we may have a very hard time convincing the process lobby (ISO26262, ISO61508) to consider using Rust in domains that seem to be the ideal fit for it from a technical merit PoV.

It's purely about the formal spec. The idea that we haven't put much effort into a spec at all yet while the formal stuff is ongoing is more of a general attitude of the team, it's not a written-down policy.

A formal language specification is from my layperson’s PoV (and I can easily get some expert opinion to be sure) - orders of magnitude easier to articulate than a formal proof of implementation correctness of the language itself.

Sure. Rust cares far more about stability than many other languages do; when we make a guarantee, we make it. Currently, forever. If we laid out a spec now, but then found out that it was incorrect, that'd be pretty bad. We don't intend to make significant breaking changes to Rust ever. As such, there are some areas that are under-specified to give us some wiggle room while we sort things out.

Overall - what I’m learning - and meaning to relay here - from professional exposure to the safety critical ecosystem, from the PoV of a processor IP silicon designer is that unless there is a practical path to a language specification we may have a very hard time convincing the process lobby (ISO26262, ISO61508) to consider using Rust in domains that seem to be the ideal fit for it from a technical merit PoV.

Yes, I totally understand this. We're just not that mature yet. These things take time. C was first implemented in 1972. K&R, a sort of informal first spec, came out in 1978. In 1983, ANSI became interested in developing a spec, and it wasn't finalized until 1989. That's six years for an informal spec, six years of active work towards a real spec. Rust is only three years old.

6 Likes

This thread loosely reminds me of a previous one along similar lines: Using Rust for railway software / [no_core]

AFAIK, I don’t think the community is any closer to a language spec/formalization than it was a year ago when that thread was ongoing.

1 Like

Yes and no. We now have two new maintainers of the reference, who have been doing a lot of work on it. We have the unsafe guidelines WG, which has been doing a lot of work lately, and that's the largest part of "unknown unknowns" in the given spec.

We have a general commitment between the lang and docs teams that we'd like to improve the reference together, though we don't have a plan yet; I'd like to make it a big focus of next year.

6 Likes

But isn’t there some subset of the language (probably a fairly large one, I’d venture) that is less contentious and more amenable to putting down as formal specification/guarantee? If I understood @microcolonel correctly, they’re not looking for a fully fleshed out one that exists today - they’re merely interested in there being a tangible plan towards getting there. So ISTM that at least starting that work with “basic” language features, ones that don’t have much debate, would go a long way towards that …

I thing going down this path will also add an extra layer of “legitimacy” to Rust, even for folks that aren’t under regulatory obligations to use fully specified languages.

2 Likes

That’s the reference.

Right, and the reference is what I also would’ve said “is the closest thing to a spec”. I suppose it’s unclear whether it is the (beginnings of a) spec and thus can be talked about as such (with the incompleteness caveat) or it’s just a side piece of documentation that may or may not exist in its current form and/or content in the future.

And so if it is the spec, how come we never talk about it as such even when people don’t ask for a complete and finalized spec? :slight_smile:

It’s not really far enough along to be good enough according to what @microcolonel needs, if I’m understanding correctly. And I did mention it :slight_smile:

Firstly thanks to everyone who’s opined! Appreciated and I’m much the better off in terms of awareness of where things stand.

@steveklabnik: I think what would be awesome is if by dialogue between:

a. folks who understand the Rust reference’s design and ambitions

and

b. folks who have been through the process of working on and with an established language specification (like the compiler architects I alluded to)

… a set of required and graded maturity thresholds could be agreed upon - for the existing Rust language reference. A kind of gap analysis but with a more formal view on what the end points should be - from the PoV of folks intimate with formal language specification.

From that point onwards, this becomes a far more tenable problem and has multiple benefits:

  • advertising the required thresholds enhances the legitimacy of the Rust language - as @vitalyd put it. The existing reference may not have what it takes but hopefully what’s needed is known and that’s a strong indicator of commitment and potential over time.

  • attaining those thresholds over time just accentuates the suitability of the language for the domains in question and buys credit from the currently seemingly wary safety themed ecosystem across different domains.

  • an essential feedback loop is established between specification designers at different ends of the formal language specification spectrum (I mean Rust and C/C++) which then becomes an interesting forcing function to steer things well.

Would there be interest in exploring this and if so who should I contact from the Rust-o-sphere ?

I work in the Arm System Software Architecture group and am very interested in at least making an initial dialogue happen between relevant parties - even if it results in an outcome contrary to what I am hoping for (because if nothing else - some important connections would be formed all the same).

Do please let me know either ways.

Thanks!

6 Likes

I certainly would love to have such a thing. I think what's most likely is, we'll end up starting a working group early next year to start to tackle that. I'll certainly be a part of it, so I can ping you whenever we decide to spin it up.

2 Likes

Excellent! :slight_smile:

I’ll stand by. I’ll also try and get some more concrete thoughts together in conversations with relevant folks here at Arm.

Cheers!

2 Likes

Just a note: As of late September, there is a Grammar Working Group whose purpose is to develop a canonical grammar for Rust, based on both existing documentation and grammar-related files within the rustc compiler. The repository where this will reside is https://github.com/rust-lang-nursery/wg-grammar.

5 Likes

Am I the only one who’s thinking the RFC Repository/process also qualifies as part of the spec?

In there, we the community discuss and specify the expected behaviour of Rust.
I guess it is spotty, because the “ancient” core of rust was developed before the RFF process existed, but all new changes/updates follow it.

Of course there is the gap between when an RFC is accepted but not yet implemented. I guess rustc is non-conformant in that time?

I would think a formal spec would only entail stable language features. (You may even want to define stability in terms of presence in the spec.) The RFC process would then be used to determine what goes into the spec, not vice versa. You certainly wouldn’t want to force everybody who aims to meet the spec to adopt any part of the RFC process (or in fact, any organizational processes), because carrying out such processes might itself prevent compliance.

1 Like

There is also the fact that some changes are considered too minor to require an RFC so just use a PR. However, from the standpoint of a safety assessment agency such as TÜV, they might be consequential.

1 Like