T-spec meeting 2025-07-31

--- title: T-spec meeting 2025-07-31 tags: ["T-spec", "meeting", "minutes"] date: 2025-07-31 discussion: https://rust-lang.zulipchat.com/#narrow/channel/399173-t-spec/topic/Meeting.202025-07-31/ url: https://hackmd.io/P79HXvkCRdKc4pcJiv9TBw --- Meeting URL: https://meet.jit.si/rust-t-spec Attendees: - Joel Marcey - Mario Carneiro - Ralf Jung - Jack - Pierre-Emmanuel Patry - Pete LeVasseur - Tomas Sedovic - Sid A - TC - Niko - Connor Horman Regrets: - Josh Triplett - Eric Huss Notes: Tomas Sedovic Agenda: - Updates to the agenda? - `t-spec` leadership update - Champions for spec-related Project goals - `t-spec` team planning - PR Review: @TC0 @ehuss ## Updates to the agenda ## `t-spec` leadership update Joel: I mentioned I was going to step down from the Spec team leadership. We have an interim volunteer: Niko is planning to take over the role for us. I will help with the transition as best I can. Niko: My intention was to help us pick a course and find a good lead to help us drive the course. It makes sense for the few months. ## Champions for spec-related Project goals Joel: Two goals were proposed: [FLS Capabilities](https://rust-lang.github.io/rust-project-goals/2025h2/FLS-up-to-date-capabilities.html): Pete LeVesseur [Expanding the Rust Reference](https://github.com/rust-lang/rust-project-goals/pull/336): Josh Triplett Joel: Niko, want to say more about what Champion means? Niko: Someone who tracks the progress and makes sure that any feedback is surfaced. For Spec in particular we may want to create some extra expectations. For more concrete goals it's nice if the extra expectations is you being a reviewer etc. This comes down to the lang-doc vs Spec. How much is the role of the Spec to actually author contect vs. do something else. ## Plan for drafting plan for language definition TC: Document describing the background and motivation of drafting a plan for the Rust language definition: - https://hackmd.io/c8WGRVutQ3GDQSHh9z51fg TC: I want to talk through the document, some of the ideas. I want to hear from Ralf about MiniRust -- where that work is, your thoughs in general. https://github.com/minirust/minirust/ Ralf: MiniRust is figuring out the nitty-gritty details for unsafe code. If you want to figure out that your unsafe code is sound and UB-free, there are things you can and cannot do. We're doing this in posts and documentations but we don't have a complete spec for that. I.e. something that documents e.g. pointer provenance, dereferencing pointers. MiniRust is my attempt at this. It's somewhat similar to MIR in terms of being the core representation. You can compile Rust to MiniRust and once you do that, there is a precise description about tree/stack borrows, provenance. Operations are precisely spelled out. It is executable so you can test all the Rust test cases. The status of this is: we just about now have all the core language features. We just got unwinding. There's nothing major missing but a long tail of small things missing. I have a student project to work on that next semester. Ralf: It's an interpreter written in a tiny subset of Rust that we're working on getting more tooling for. It's made to look like Rust so Rust programmers can read it. It's done in the literal programing style. I've been working on this for a few years with the goal to some time contribute this to whatever the official thing is. Pete: Thanks for this efficient description. You said this is being done outside the scope of the Project. What does it mean? Ralf: I created a repo on github and worked on it. I intentionally did this outside of Rust and invited my students to work on it to be able to move forward quickly. Pete: How is MiniRust connected to t-opsem? Ralf: MiniRust is my project. But ultimately if you look at what T-opsen was chartered to do, MiniRust is an option to get there. TC: Mario and I talked some. Can you please talk about the way the language definition can be scoped? Mario: I've been thinking about this from the perspective from someone eyeing soundness theorem (via a proof). Something I think we should strive for. The soundness theorem: Safe Rust programs don't have undefined behaviour. We need to define: what is a safe Rust program and what is undefined behaviour. For Rust programs: what what are the correct input programs, things that would count as legal Rust programs. The typechecker can only say yes for all the behaviours the typechecker allows. Same for traits instead of types. There's borrow checking, initialization checking, etc. All of the static semantics of a Rust program. You know the program was accepted by the Rust compiler. Mario: In rustc that generates MIR. Now we need to lower it to MiniRust. There's no code that supports lowering right now. We need a formal definition of what the lowering is. That would mostly add parameters for all of the ways that you can lay out structs, where you can place the fields etc. Once you have that, you're basically there of describing from the front-end to the backend (MiniRust). And MiniRust has the execution semantics. Mario: Having all that stuff formally isn't something I insist on but it should be written in some kind of machine-readable program. TC: How do you see the relationship between the formal side and the presentation of it that's accessible to the humans too? Mario: I've been inspired by the WASM spec. And the JavaScript spec has been doing something simirlar. You have an itemized list of rules and you have something similar written in a formalistic style and a back-and-for between them. A description and a formal text and they both mean the same thing. They're both authoratative. If they mismatch, that's a bug in the spec. You can put that in a PDF document. TC: Ralf, what does a complete spec means to you? Describe the document we would end up with. And how do you think of this in terms of a research program -- what it would look like and how we would go about producing this if we had a team to do it. Ralf: The complete spec should say whether a given program has undefined behavior or not. Take the program and the spekc together and answer that question. I'm focusing on UB because that's the hard part. There's a lot of specs that do reasonably well on the happy path but when it comes to whether something is in UB, it's really ambiguous. Which is why I proposed MiniRust for this. Ralf: It would need both the lowering Mario mentioned and actual semantics of the language. They would say what the semantics of the experessions are. In terms of a research program I'm writing a proposal. In terms of the spec there's much more figured out than written down. It's not even that long. The big one is the aliasing model, then there's the concurrency model. If we ignore those two, the list of actual unanswered questions is fairly small. Ralf: The research program is less about figuring the spec out and more about taknig the answers we already have and turning it into a document that serve all the people it should serve. TC: How would you see that part of the program going? Ralf: I haven't given that much thought to lowering. For MiniRust I'm not sure: you could literaly take the MiniRust code and add more text there. Some of it you actually want to have in the code form (rather than in English) in the spec. What JS/WASM folks do is they have enumerations with English sentences but they follow a regex that basically turns English into a formal grammar. I think I'd prefer code. Ralf: I spoke to those folks because they were interested in doing something like that for Rust: https://pure.kaist.ac.kr/en/persons/sukyoung-ryu Mario: I floaded this concept of "undecided behaviour" in order to express the open questions we have. To decouple the spec writing process. I want to avoid the spec waitng for us deciding everything in the language. Let's say theres' a corner of the language that's not been decided (like union validity rule) how well can that be expressed in MiniRust. Ralf: It's easy to add an undecided expression. You'd probably want to do some post-processing because the undecided thing can't run. Mario: So if there's a choice of a finite number of options, you'd use a flag to select one? Ralf: Yes, or you could use some sort of determinism. We do this for the memory model. We have a trait that has "load" and "store" and the rest of the code use them and doesn't care what the memory model is. We have two models currently. TC: Niko, what are some fo your thoughts? Niko: Everything that was said makes perfect sense to me. There are some things are similar for the type system. At least initially it'd be great if the spec was doing more of the job defining variance etc. The first thing I'd want to certify (especially for safety-critical) would be knowing what properties you'd like to demonstrate. I want to understand better the consumer side. What do the customers of the spec want. Pete, I understand the safety layer comes later than where most companies are with Rust. But I don't know how close we are. Pete: (safety critical context). There are many domains, I can't speak to all of them. Automotive I know best. For automotive there's a lot of code that needs some sort of ASIL rating. There's "QM" (quality managed) -- the smallest level. From there you have A, B, C, D. As you progress, you get higher levels of criticality. ASIL QM might be software running on the head unit. The thing that you plug your phone into and therefore mostly don't use most head-unit code in. B: Safety system for automated driving/ADAS, camera D: Can result in loss of human life. Things that are closest to executing actuation on the vehicle: steering wheel, pedal, etc. Pete: Typically you need three things: safety-qualified compiler (e.g. adacore, ferrocene), any library you use must be safety-certified, and coding guidelines. These are ideally based on something real from the language. The one used in safety critical is MISRA. It's been proven in court to be a legal defence against loss of life. The coding guideline is what we're trying to build in the safety critical consortium. Niko: What are the next things that would broaden the scope? Pete: ASIL QM up through ASIL B may be already covered by the existing FLS. A lot of safety critical is belt and suspenders approach. You try your best and they typically fall short, so you have some suspenders to catch you. Maybe the compiler and spec is not perfect but maybe we have tests. There's a big leap from ASIL B to ASIL C or ASIL D where there's a lot more formalism expected by assessors and the standards. Pete: In safety critical industries you may have piece of hardware that runs maybe 10 lines of code, but it's ASIL D. The cost of code per line grows exponentially. It is extremely expensive. So therefore hardware and software are architected to minimize the lines of code that are higher ASIL levels. Niko: One of my hopes is there's a lot of opportunity to lower the line-of-code cost. Pete: What I've heard from people in the industry is they're trying to hit as much ASIL QM as you can. And that's basically just following the coding guidelines. TC: AS you get to ASIL B, C, D -- does it start to overlap with the verification community? Pete: I'll ask more questions, but my understanding is that yeah as you get to C and D you have to show mathematical proofs to show your software is correct. Mario: T-spec recently got the FLS. What exactly does maintenance of that entail? I know we want to update it to the latest Rust version. But what exactly needs to be in there, needs to be omitted? My perspective is: it's kind of vague in certain places but it's not clear where you can be vague. And you described it as a sort of box-ticking exercise. How exactly do the requirements on the document impact T-spec. Pete: What you must do is get an assessing company somewhere to sign a document saying you're good. You need to convince someone / a group of people. There was likely a work being done by the FLS folks and an assessor and they probably made intentional choices about what to specify more or less. But in the end, you need to have something to convince someone out there. There's a distinction between software certification and tool qualification. What Ferrous did was a tool qualification of the compiler. Pete: One more thing: in the future there's this hope that we can have a harmonized document that would describe the language that would be useful for certain domains e.g. safety critical. There is some tension there. E.g. having more formalism would benefit C, D etc. But I don't know how much the Rust community would react to us asking to stop making changes to the harmonized document as it's now going through qualifications. Pete: There's a cost component to the qualification and a timing aspect. TC: There's a subset of a safety critical community which wants us to update the FLS in a minimal way and keep doing that forever. Is that accurate? Pete: I'd say that may be accurate for ASIL QM, maybe A and B as well. Niko: Can you restate this? TC: There's a subset of a safety critical community that mostly wants us to keep the FLS in its current form. Update it minimally with changes for rust. And provide an assurance that we will keep doing that. Niko: I think what's missing from that statement is libraries. Not ever covering libcore is a crucial gap. TC: Does the standard library documentation serve the need of safety critical at all? Pete: How ferrocene was produced, you could imagine that there was a similar process for say libcore. We want to safety-certify certain parts of libcore. Where we look at what exists today in the Rust official docs for libcore and std and if possible enrich it. If not, provide a separate document to assessors. But the dollar cost per line of code is expensive. Tension between commercial and open source. Ralf: Pete, is there some world in which the Rust project produces a document of sorts that does its best describes what the safety of the language is. And the reassessments are downstream of the document? There are many people who would like to see a Rust spec and many of them are not in safety critical. Niko: I don't feel we should be directly talking to assessors. That's more job for ferrocene and other toolchain vendors. But we should be conservative of changing text to make their lives easier. That also aligns with what I talked to Florian Gilcher. Pete: I agree with what Niko said. The document can be changed dramatically over time. But what folks would like to see is chain of custody. At this state we can still safety-qualify the Rust compiler using the document in its current state. If there is some harmonization process in the future, we can figure it out together how to do it correctly. Mario: Maybe what we want to do with this is to keep the FLS as is for a while. We add a few things but only corresponding to compiler changes. And then we're also working on a 2.0 document that's trying to satisfy our other goals. And at some point in the future merge them. Trying to incrementally move the FLS sounds crazy. Niko: That strikes me as the maximally expensive way of going about this. Something for further discussion. Ralf: How do we extend the FLS incrementally? Niko: You can add new things and those are essentially free. If you have something that depends on paragraphs A, B and C, we can add more so long as we don't modify those three paragarahps. Pete (in chat): Yes, this should be possible, since each paragraph and section has their own tagged ID. Ralf: It feels like it would add a huge amount of friction having to work with a document. Niko: What takes a lot of friction is developing safety critical code without a spec. We were given this. Ralf: If this slows down the actual spec work, that's not a gift. Mario: Let's say we have FLS in the maintenance mode. And we're building the V2. If we can construct a document that does an exact mapping between FLS and the new doc that might get past the assessment. Niko: I think the approach I'd like us to take is a more of an experimental one. Let's try a few different things and see and iterate. We want a process that works for the Project and a process that ideally moves us with as much incrementality as possible. And usually we don't get that without trying things. Pete: I do think we can do the experimentation while keeping the existing work, but carefully. Pete (in-chat): We can specify this as being one of the t-spec FLS sub-goals to figure out how to incrementally start adding bits of formalism by discussing with companies that are current users of the FLS on what would/would not impact them. Niko: What I'm saying is: let's take a specific thing: extending an area of the FLS in a differnt way. And have e.g. three prototypes. We did something like this earlier. I'd like to see the fresh ideas for a v2 spec. Mario: I do know there are some things that are in the spec. And we want to have those and also have the FLS. Niko: Maybe we should look at the FLS. Try adding them to the FLS and see if it's a bad idea or not. TC: I felt one of the outcomes of this meeting is trying to understand there's the safety critical community and then there's more. The FLS covers ASIL QM to B. But then there's the rest. I don't think we're leaving the safety critical community behind by talking about spec. Niko: I worry we're leaving behind some of the earlier adopters. How smooth of a path can we chart? The FLS is out there, does the job, I don't think we need to put it in a maintenance mode right away. ## PR Review (Not happening today.) ## Jitsi Chat https://hackmd.io/P79HXvkCRdKc4pcJiv9TBw 8:03 PL Pete LeVasseur Pete LeVasseur says:The not-so-nice, but very evocative way of phrasing this might be what this role is called pejoratively in Automotive: "beater-and-tracker" ;D 8:07 Pete LeVasseur says:This title is usually bestowed by software engineers behind closed doors when the PMs are not present 😄 8:08 R Ralf Ralf says:😄 8:08 PL Pete LeVasseur Pete LeVasseur says:I personally would appreciate some context 8:09 Pete LeVasseur says:Feel free to drop links for me to read later too ("read this newb") 8:09 N nikomatsakis nikomatsakis says:FYI-- today in particular I have another meeting at 11:45am 8:10 PL Pete LeVasseur Pete LeVasseur says:👏 8:13 Pete LeVasseur says:I'm raising my hand, take your time 8:14 Pete LeVasseur says:Don't mean to interrupt 8:15 Ralf Ralf says: https://github.com/minirust/minirust/ readme has link to video at the top 😃 8:15 what they are doing in JS: (also shows some very cool tooling) https://www.youtube.com/watch?v=Mu8pQbs9NvA&list=PLyrlk8Xaylp7MV2EwJi6xZc95YSG-uI-b&index=8 👍 8:24 Ralf says:wasm: https://www.youtube.com/watch?v=-rRTsG29j-Y&list=PLyrlk8Xaylp7MV2EwJi6xZc95YSG-uI-b&index=10 👍 8:24 Pete LeVasseur Pete LeVasseur says:I'd like to raise a topic regarding safety-critical, but don't want to interrupt, so feel free to find a good space in the conversation to let me in. 8:28 N nikomatsakis nikomatsakis says:point of clarification rust: which people specifically are you referring to? 8:31 R Ralf Ralf says: https://pure.kaist.ac.kr/en/persons/sukyoung-ryu 8:32 PL Pete LeVasseur Pete LeVasseur says:❤️ 8:36 nikomatsakis nikomatsakis says:(have to drop, thanks all for the thoughtful conversation) 8:49 nikomatsakis nikomatsakis says:I lied, I have a few more minutes 8:51 Ralf Ralf says:wb 😃 8:51 Pete LeVasseur Pete LeVasseur says:Sorry for the heavy change in topics to safety-critical. Maybe we can let TC bring us back on track? 8:59