this post was submitted on 12 Nov 2024

45 points (100.0% liked)

Rust

111 readers

4 users here now

Welcome to the Rust community! This is a place to discuss about the Rust programming language.

Wormhole

!performance@programming.dev

Credits

The icon is a modified version of the official rust logo (changing the colors to a gradient and black background)

founded 1 year ago

MODERATORS

snowe@programming.dev

Ategon@programming.dev

EdTheLegendary@programming.dev

kahnclusions@programming.dev

torcherist@programming.dev

Rust needs an official specification (tweedegolf.nl)

submitted 4 days ago by snaggen@programming.dev to c/rust@programming.dev

12 comments fedilink hide all child comments

top 12 comments

sorted by: hot top controversial new old

[–] BatmanAoD@programming.dev 2 points 2 days ago

This article somehow links to both the Reference and the Ferrocene spec, but still concludes that an official non-Ferrocene spec is necessary.

Why doesn't the Ferrocene spec accomplish what the author wants? He states:

In other words, without a clear and authoritative specification, Rust cannot be used to achieve EAL5.

What? Why can't the Ferrocene spec (and compiler) be used? Do Ferrocene and TÜV SÜD not count as "some group of experts"?

(Regarding the author's opening paragraphs, the Reference does make the same distinction about drop scopes for variables versus temporaries, though I can see why he finds the Ferrocene spec clearer. But that doesn't demonstrate that the Reference is useless as a stand-in for a specification.)

[–] FizzyOrange@programming.dev 16 points 3 days ago (1 children)

It's not because we have tested this program extensively on every C++ compiler, but because the language rules of C++ say so.

Debatable. Saying things in a prose specification doesn't magically make them happen. Tests and reference models can though.

I also don't really agree with the SIL requirements that languages need to have rigorous specifications to be safe. Clearly it's better if they do, but would your rather fly on a rocket controlled by C code or Rust code?

IMO a specification would be really nice to have, but it main purpose is to tick a certification checkbox, which is why the only one that exists was written specifically for that purpose.

[–] copacetic@discuss.tchncs.de 11 points 3 days ago (2 children)

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.

[–] BatmanAoD@programming.dev 1 points 2 days ago

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.

[–] FizzyOrange@programming.dev 7 points 3 days ago (1 children)

you can say that without a spec as well but what does “wrong” mean then? It just means you personally disagree with its behavior.

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.

[–] copacetic@discuss.tchncs.de 5 points 3 days ago (1 children)

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.)

[–] FizzyOrange@programming.dev 5 points 2 days ago* (last edited 2 days ago) (1 children)

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.

[–] copacetic@discuss.tchncs.de 3 points 2 days ago

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.

[–] onlinepersona@programming.dev 3 points 4 days ago (3 children)

I'm actually surprised there is no specification. It's how I thought languages were written: spec first, implementation later. Do RFCs serve this purpose?

Anti Commercial-AI license

[–] BatmanAoD@programming.dev 4 points 2 days ago

That's actually not how any language has ever been written, though it's easy to get that impression from how much the C and C++ communities emphasize their formal specifications.

But in fact, both languages were in production use for over a decade before they had a formal spec. And languages with formal specifications are actually a tiny minority of programming languages.

[–] snaggen@programming.dev 10 points 3 days ago* (last edited 3 days ago)

That requires a complete picture and all possible use cases from the start. Initially when a language is new and hardly used there are much to benefit from flexibility and trying new concepts. Then as the language matures, a more formal process is needed to ensure stability. There is a reason these discussions comes now, since rust is in a very stable phase.

[–] copacetic@discuss.tchncs.de 6 points 3 days ago

Welcome to the real world. /s