T-spec meeting 2024-09-26

--- title: T-spec meeting 2024-09-26 tags: ["T-spec", "meeting", "minutes"] date: 2024-09-26 discussion: https://rust-lang.zulipchat.com/#narrow/stream/399173-t-spec/topic/Meeting.202024-09-26 url: https://hackmd.io/PbcQZcsFS0KYjWBfqGvTaQ --- Attendees: Joel Marcey, Connor Horman, Pietro, Eric Huss, Monadic Cat, pnkfelix, TC, Josh Triplett, Sid Askary, Alexandru (CEO of OxiOS), carbontaniumam, theemathas Agenda: * Spec discussion with safety-critical representatives * Gaps between Ferrocene and the Reference ## Spec and Safety Critical Discussion Thank you to Alex for taking time to join us. Alex from OxidOS introduced himself. Joel provided context as to why we invited Alex. Alex: Indirect user of the spec. Need to deliver software to the customer. Customers ask for a spec that they can use to be certifiable. And OxidOS is not able to deliver that to them. Alex: Two specs could cause a tools problem. Some vendors will be using the Ferrocene spec. Some vendors would use a non-Ferrocene Rust specification. TC: What if a tool vendor offers a qualified product based on Ferrocene and another tool vendor provides a qualified product based on a t-spec Rust specification? How does that affect your work? Alex: Documentation is the key. It would be very difficult to certify a toolchain based on tools that use two different specs. Alex: Switching from the FLS to a Rust specification from the t-spec team would require a cost to prove compatibility. Connor: Can qualified tools be made available by the Rust Foundation? Pietro: Liability will probably prevent that. Pietro: Ferrous doesn't want to maintain the FLS. Pietro: Switching to the Rust spec from the FLS for Ferrous unless it is exactly the FLS will be very costly. pnkfelix: If `t-spec` produces spec tomorrow, would customers using FLS actually move to it? Alex: They may not. Even if a qualified compiler came out tomorrow on the new spec, it may not make business sense to move from the FLS. Alex: Even if `t-spec` produces an official spec, it may not help certain companies because there will be a business cost. Because FLS is already part of the toolchain. It's the only option. Alex: OEMs need a reason to swtich from C to Rust. The main reason for a switch is lowered cost (*not* "memory safety" on its face). C is super expensive. The reason to convince them is that you don't need all the tools from C. But we need documentation and a spec. *Felix summaries Alex's outline: there rules in MISRA (or ISO 26262?) that demands certain checks are done. Part of the cost-saving argument here is a document that takes a large number of those MISRA rules, and for each one, maps it to a corresponding set of rules **in** the FLS and shows how Ferrocene (i.e. Rust) obeys that rule without using a separate tool.* Alex: The Rust Project producing a spec would be clear signal to the safety critical industry of its seriousness. Pietro (in response to TC question about what aspects of a spec matter most, beyond it having qualified toolchain vendors): It's imporant to recognize that the toolchain vendors themselves are the customers who care about the test traceability matrix, because that it then *used* as part of the qualification process during the argument to the assessor. Once the tool has been blessed by the assessor, the end programmer itself does not tend to care about the presence/absence of a test traceability matrix. Sid: Chip and hardware manufacturers are also a key component here. They need a spec to ensure chip compatibility. Maybe having someone from ARM would be good to talk to. Alex: It's more the Tier 1 suppliers that matter. ## Ferrocene and Reference Gaps https://hackmd.io/@chorman0773/B1Gx66Z0A/ Josh: We shouldn't block putting something into the spec that's accurately describing current behavior just because `t-lang` hasn't reviewed it yet; that's historically been a rate-limiting problem for the reference. We should be able to document things descriptively; if the spec surfaces surprising behavior, we can always choose to improve the language later. TC: There's a caveat there. There are a lot of places where things can be documented even if they're surprising because they can be checked against rustc. But there are other places where documenting such things amounts to a guarantee about the language, and those need to be elevated to lang. There are many opsem and some types things there. This comes up often in Reference reviews. Josh: +1. That's an important caveat. Joel: Did you do any correctness checking? Connor: No, noted some mistakes as I found them, but nothing comprehensive. ## Alex from Oxide OS Alex: CEO of OxidOS Automotive, they're building TockOS that's meant to be used in automotive and other spaces. Alex: We are an indirect user of the spec. We want to certify an operating system. Most probably the spec is used by the compiler provider. I'm not an expert in certification here. Alex: We need the spec yesterday because we need providers who will be able to provide us tools. Pietro: ISO 26262 is the automotive safety standard. ## Meeting Chat (from Joel's Chat) Monadic Cat Monadic Cat says:Jitsi works in Firefox, yeah. And I can't imagine it doesn't work in Chrome 8:04 Monadic Cat says:Hey Pietro, can I ask, for the users of the FLS, would the introduction of the UB that comes from provenance and stuff into the FLS cause a major headache? Like, are certifications happening under the presumption that the listing of UB in the FLS is exhaustive or...? (I don't see provenance mentioned at all in the FLS, though please do correct me if I'm wrong and just missed it.) 8:08 me says:Alex should be here within 5 minutes. 8:09 me says:Daniel just told me he is stuck with a customer and can't make it. 😦 8:09 P pnkfelix pnkfelix says:or perhaps T-types. (Or both, not sure.) 8:09 avatar Josh Triplett Josh Triplett says:👍 8:11 avatar Eric Huss Eric Huss says:is anyone taking meeting notes? 8:13 MC Monadic Cat Monadic Cat says:Specifically, on making it approved to be normative: having documentation which is labeled "descriptive and not normative" would be good 8:14 Monadic Cat says:So the things that are enforced need to be known, but specifically how it does it doesn't need to be specced? (trying to understand pietro's remark) 8:16 P Pietro Pietro says:Yes. 8:16 me says:Hi Alexandru! 8:23 me says:Alex - here is where we are taking/minutes notes for the meeting: https://hackmd.io/PbcQZcsFS0KYjWBfqGvTaQ 8:23 A Alexandru Alexandru says:Hi, sorry for being late. 8:23 MC Monadic Cat Monadic Cat says:Hello! 8:23 A Alexandru Alexandru says:small issue with my kid 😃 8:23 P Pietro Pietro says:ISO 26262 is the automotive safety standard btw 8:30 MC Monadic Cat Monadic Cat says:What does compatibility look like here? 8:31 Monadic Cat says:I think this is a question for Alexandru. 👍 8:32 me says:The major issue here is that the FLS will become the de-facto specification for certification. And tool vendors will use the FLS in their qualification efforts. 8:36 me says:There is no `t-spec` spec that they can use. So that is all theoretical. 8:36 me says:The Rust Reference-based spec does not exist at this point. 8:37 MC Monadic Cat Monadic Cat says:It's not clear at all to me. People keep saying that the FLS and the spec produced by the Rust Project officially need to be compatible, but it has not actually been said by Pietro or Alexandru what is required for that compatibility to exist. ❤️ 8:39 avatar Josh Triplett Josh Triplett says:(Side note: somewhere around 5-6 years ago, I did an analysis of MISRA-C to figure out which rules would sensibly apply to a MISRA-Rust. That work was internal at a company and never public, but I'd be happy to do it again at some point.) 8:40 avatar Connor Horman Connor Horman says:Yeah? Do they have to provide the same legality rules? I'd expect that if the legality rules differ, then that's a problem with the FLS because the FLS is documenting legality rules that aren't part of the language (assuming a complete Reference-spec on our side). 8:40 me says:The spec is basically the beginning of a long-line in the certification process. 8:44 me says:So if you replace the specification in that process, you have to propogate that work in the steps after it. 8:45 me says:Which is why it would behoove us to ensure that (1) the FLS is actually correct as it relates to documenting rustc (2) Any spec we produce is compatible with the FLS. 8:46 me says:Because like it or not, vendors are going to use FLS. We can't stop that because we don't have a spec right now and they have a business to run. 8:46 avatar Josh Triplett Josh Triplett says:(And even if we *have* a spec, they may still use the FLS if it meets the needs of certification or other uses better.) 8:47 me says:👍 8:47 P pnkfelix pnkfelix says:bingo: liabilty 8:49 Optimally, the Rust Project would take over the FLS to maintain, whatever that means in practice. 8:52 me says:It may have the same level of detail, but presented in a different way -- that would also cause problems with the assessor, if I understand correctly 8:59 P pnkfelix pnkfelix says:this confirms suspicions I have had about this matter Monadic Cat Monadic Cat says:This is a lot to chew on. I'd like to thank Pietro and Alexandru for their help here, I think it's been very illuminating 👍 Josh Triplett Josh Triplett says:(I wouldn't expect evolution of FLS to be of the form "FLS doesn't match the language in some major area"; I'd expect evolution of FLS to be of the form "we want the style of the spec to be useful for more goals than just certification".) pnkfelix pnkfelix says:yeah that's a horrible business risk. But wouldn't we have the advantage of "officiality" in that case. Anyone could fork the spec, and we can't stop that, but we would be the *official* spec. 9:15 P Pietro Pietro says:(I wouldn't say FLS was forked from the reference, we took a lot of content from it, but it was written from scratch) Me: +1 Alexandru 9:16 But if we adopted the FLS as the Rust spec of record right now, then the likelihood of that divergence of a few business sticking with the FLS becomes very small. 9:20 Monadic Cat Monadic Cat says:It sounds to me like the FLS would be willing to evolve a little bit to make an implication that "certification under the FLS implies certification under the Rust Spec" so we can end up having that in a certified document, so the chain of certified implications gives everyone a migration path? 9:20 Connor Horman Connor Horman says:Based on this, I'm not quite sure that's true, because we may not just be talking about the FLS. 9:20 The Rust Project losing control of the Rust specification would be the worst case scenario, imho. 9:25 Monadic Cat Monadic Cat says:hrm 9:27 pnkfelix pnkfelix says:mmm 9:29 Josh Triplett Josh Triplett says:👏 9:31 26262 9:31 The goals of the Rust specification as was agreed to in the RFC that Mara wrote are to correctly document rustc and provide support for the safety critical industry (those are literally in the motivation section of the RFC). The question before us is how important that second goal is for our work starting today. 9:37 Josh Triplett Josh Triplett says:Felix: ❤️ 9:54 MC Monadic Cat Monadic Cat says:I'm not a T-spec member, and I sorta missed the meetings/conversations where adopting the FLS was decided against while adopting the Reference was agreed upon. But yeah, it does seem to me like if we're willing to migrate the Reference this way, we should be willing to do it with the FLS instead, and there seems like rather large benefits for doing so 👍 9:55 Monadic Cat Monadic Cat says:it is real difficult to communicate about this ngl 10:02 SA Sid Askary Sid Askary says:Safety critical is the realm of Safe systems programing languages (i.e. Rust). It is natural that their use case is timely. 10:02 avatar Josh Triplett Josh Triplett says:I wouldn't expect it to be "minimal review" either; I'd expect it to take review, but that's review that we could *do* if we actually started doing so. 10:02 MC Monadic Cat Monadic Cat says:So... what *would* it take to bring the FLS under the control of the Rust Project, anyway? 10:03 Me: s/spec of record/document of record to produce a spec 👍 10:05 Connor Horman Connor Horman says:(FTR, I would like to get off clock *soon*) 10:06 P Pietro Pietro says:same 10:06 avatar Connor Horman Connor Horman says:(BTW, the jitsi partinpants tab shows the order hands are raised) 10:09 me says:If I ever came across in my words implying that I think we should adopt the FLS as-is and then call it day and disband `t-spec`, I apologize. That was never my intent. 10:09 If I ever came across in my words implying that I think we should adopt the FLS as-is and then call it day and disband `t-spec`, I apologize. That was never my intent. 10:09 me says:Having two different versions of a spec that are equivalent in normative content (even if one is a superset of another), but serve different purposes, I think is ok. 10:11 me says:I just don't want to get to the point that the FLS is out there being used as an authoritative thing that the Project has no input over. 10:12 avatar Connor Horman Connor Horman says:(I'm hard out at :15, when I roll over to 2.3 hours) 10:12 Josh Triplett Josh Triplett says:TC: I think it's very reasonable that a company may not be willing to do the "same work under the Project banner" if the Project has repeatedly rebuffed that in the past. 10:17 👏 10:17 P pnkfelix pnkfelix says:yes thank you very much Alex 10:17 T TC TC says:Josh: Agree. 10:17