James: coming from background in safety critical areas
fairly tied to“qualified tool chains”
looking for a lang that is well-specified
confidence that the program will“do what you intend” but also you need a long lifetime
e.g. planes are still in use after 30-40 years
would want a toolchain that can last that long
always hoped Rust could be a good language for these areas
Safety yay!
but still some work to go
this is a large set of work that is not necessarily useful outside of this scope
don’t want to put a burden
Scott: and having a company/entity that is doing that long-term support would be useful regardless
Yes. and having a company is a particular plus.
Ralf: some of the goals are quite well-aligned with the project, though, right? e.g. a spec
James: yes, also a test suite for that spec
overhead is probably more things like paperwork, validation against spec
non-goal: forking the language :)
Ralf: as an academic, I have ideas of what I have in my head when you say spec, but I’m curious what kind of spec is needed for safety critical and to what extent would academic collaboration be useful
James: safety critical spec. spend a lot of time talking about what your application needs to do
but guidance on“tool qualification”(certifying your tools) is very vague
need to have a“level of confidence” that it will“perform to level that is necessary”
Historical specs are very prose-driven(e.g., C, Ada, etc)
but we are thinking of something more“machine driven”
but we should be pragmatic, maybe we can isolate some parts(e.g. borrow checker) and prove properties about them
lean on academic support where possible
Centril: some parts of compiler seem like they could be formally specified(e.g., the“AST validation” step, using e.g., denotational semantics)
Ralf: the operational semantics contains large fragments that wouldn’t be that hard to specify
James: we also have the ability to“subset” the language
we might say“you can’t do that in sealed rust” to start
or we can add custom rules like“if you use unsafe code you must follow this checklist”
end-engineers can have the requirement to check certain requirements
this is what MISRA C is, essentially
hope is that“safe sealed rust” is kind of like“MISRA Rust”
and unsafe might opt into a checklist or something
Centril: when adding unstable features, usually very easy to check if they are being used, but if you were trying to subset the language for stable features, that would be harder
James: goal would be that“sealed rust” is sort of a“very slow channel”, though I’m not sure how that is best achieved(e.g., slower than stable)
Centril: you could use a #[sealed] attribute in stdlib or something like this to“opt-in” to stability at the“sealed” channel level
James: process I see is before you apply sealed attribute, you need to have specification + validation work done
this means we can take new features and do that work to include feature X in the next sealed release
“anything we want to include needs to opt-in to this level of specification”
some things can be harder to isolate
Ralf: is there a risk that some“old component” would have to live in compiler for 3 years… or something?
James: I expect to have one sealed rust major release“per edition”
James: I’d expect that something like NLL vs polonius would be more of an impl detail without necessarily changing the spec of what programs are accepted
James: I expect long-term support for sealed rust to be done by external funding
Links
Minutes/notes