Can we currently reason about Rust code with absolute certainty? Not really, but we should be able to. In this article, we dive into the reasons why it may be time for a Rust specification.
The specification does not make anything happen but it enables you to say “the implementation is wrong”. Of course, you can say that without a spec as well but what does “wrong” mean then? It just means you personally disagree with its behavior. When “wrong” means “inconsistent with the spec” everybody involved can work with more clarity and fewer assumptions. Wrong assumptions can kill people flying rockets.
You can say the Rust implementation is wrong if it doesn’t conform to the Reference. That is not the same as “you personally disagree with the behavior.”
Rust’s guarantees about the behavior of safe code are far stronger than anything C or C++ provides, with or without a formal spec.
In SIL world, the C++ issues would not be considered bugs but maybe change requests.
The SIL philosophy (as far as I know it from ASIL) is “unsafe unless convinced otherwise”. That seems like a good idea when the lifes of humans are on the line. Without a spec how would you argue that a system/product is safe?
(Aside: Software in itself cannot be safe or unsafe because without hardware it cannot do anything. Safety must be assessed holistically including hardware and humans.)
would not be considered bugs but maybe change requests.
That’s just playing with semantics. They are clearly bugs. They are literally called “defect reports”.
Without a spec how would you argue that a system/product is safe?
Lots of testing, including randomised testing and ideally formal verification.
Comprehensive test coverage - both code coverage (lines, branches) and functional coverage (hand written properties).
Functional safety features (ECC, redundancy, error reporting & recovery, etc.)
Engineering practices known to reduce the chance of bugs (strong static types, version control, CI & nightly tests, rigorous engineering processes - requirement tracking and so on, and yes ideally well written specifications for all the tools you are using).
There are many aspects to safety and it’s definitely a good idea to have a spec for a language, but it doesn’t automatically mean safety is impossible without it.
Software in itself cannot be safe or unsafe because without hardware it cannot do anything.
The nice thing about abstraction is that you can talk about software without considering the hardware, more or less. If one says “this software is safe”, it means it’s safe assuming it’s running on working hardware.
It doesn’t always hold up - sometimes the abstraction leaks, e.g. for things like spectre and rowhammer. And there are sometimes performance concerns. But it’s pretty good.
You definitely can do without a language spec. I heard in aerospace another approach is common: They use whatever compiler and then verify the binary. That means different tradeoffs of course.
Fair enough. In practice, we resolve it recursively with a higher level specs and at some point it is just “someone wants that”. In commercial software development (where SIL is used) that is a customer who pays for it or some executive.
The specification does not make anything happen but it enables you to say “the implementation is wrong”. Of course, you can say that without a spec as well but what does “wrong” mean then? It just means you personally disagree with its behavior. When “wrong” means “inconsistent with the spec” everybody involved can work with more clarity and fewer assumptions. Wrong assumptions can kill people flying rockets.
You can say the Rust implementation is wrong if it doesn’t conform to the Reference. That is not the same as “you personally disagree with the behavior.”
Rust’s guarantees about the behavior of safe code are far stronger than anything C or C++ provides, with or without a formal spec.
Nope. Specs can have bugs. Here are the bugs in the C++ spec for example:
https://www.open-std.org/jtc1/sc22/wg21/docs/cwg_toc.html
As I said, specifications are useful and desirable, but the SIL’s dogmatic “no spec = unsafe” is clearly not based in reality.
In SIL world, the C++ issues would not be considered bugs but maybe change requests.
The SIL philosophy (as far as I know it from ASIL) is “unsafe unless convinced otherwise”. That seems like a good idea when the lifes of humans are on the line. Without a spec how would you argue that a system/product is safe?
(Aside: Software in itself cannot be safe or unsafe because without hardware it cannot do anything. Safety must be assessed holistically including hardware and humans.)
That’s just playing with semantics. They are clearly bugs. They are literally called “defect reports”.
There are many aspects to safety and it’s definitely a good idea to have a spec for a language, but it doesn’t automatically mean safety is impossible without it.
The nice thing about abstraction is that you can talk about software without considering the hardware, more or less. If one says “this software is safe”, it means it’s safe assuming it’s running on working hardware.
It doesn’t always hold up - sometimes the abstraction leaks, e.g. for things like spectre and rowhammer. And there are sometimes performance concerns. But it’s pretty good.
You definitely can do without a language spec. I heard in aerospace another approach is common: They use whatever compiler and then verify the binary. That means different tradeoffs of course.
A specification is just another form of implementation that suffers from the very same problem you describe too.
Fair enough. In practice, we resolve it recursively with a higher level specs and at some point it is just “someone wants that”. In commercial software development (where SIL is used) that is a customer who pays for it or some executive.