3 ms·
> Publish a formal language standard first. You don't need a formal language standard to make Rust usable for safety-critical areas. You do need a formally spe
by lifthrasiir 2y ago
> Publish a formal language standard first.
You don't need a formal language standard to make Rust usable for safety-critical areas. You do need a formally specified language for the certification, but it doesn't have to be official because heck, you need much more than a mere formally specified language anyway as you've just said. An expanded version of Ferrocene would just fit the bill for example.
I think some people are obsessed about the "formal" specification or the language "standard" because they are misunderstanding their effects. They are absolutely nothing without additional supports. A "formal" specification in this context is not really mathematically formal (like, say, WebAssembly [1]); it merely means that a specification is written in clearly defined terms and logically decomposable statements. A language "standard" is useless if it isn't or can't be enforced, and it doesn't even require the (non-mathematical) formality (though most standard organizations would demand that). As for now, the Rust language specification is "formal" and "standard" enough to be useful for language users, while it remains useful for third-party implementors but they can still find some gaps here and there.
[1] https://webassembly.github.io/spec/core/ https://webassembly.github.io/spec/core/
- nextaccountic 2y agoThe linked spec of wasm is written in English. Can we even say it's "formal"? Did anyone specify wasm using something like Coq, Lean or Isabelle/HOL?
- steveklabnik 2y agoI agree that people mis-use the “formal” word when it comes to specifications. But on this specific question, https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verifying-the-webassembly-specification.pdf https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verif... is the work I am aware of.
- lifthrasiir 2y agoWebAssembly is specified in an English prose and a formal notation, as you can see from, for example, [1]. It is still true that a (mathematically) formal specification can suffer from bugs due to the lack of verification, but it is much easier to verify an already formal specification than a prose specification. It is also possible to turn a prose into a formal specification if the prose in question is already close enough to the formal notation, like ESMeta [2]. [1] https://webassembly.github.io/spec/core/valid/instructions.html https://webassembly.github.io/spec/core/valid/instructions.h... [2] https://github.com/es-meta/esmeta https://github.com/es-meta/esmeta