4 ms·

Sincere question, I didn't realize that Rust didn't have a specification. How can folk say Rust guarantees safety when it doesn't guarantee an implementation? I

Sincere question, I didn't realize that Rust didn't have a specification. How can folk say Rust guarantees safety when it doesn't guarantee an implementation? I don't see how you could have one without the other. Now, admittedly, the lowest level language I've used is Go!, so fairly abstracted (and no memory management), so I might be mistaken, but it doesn't seem like you can have safety without a specification.

steveklabnik 8y ago
> How can folk say Rust guarantees safety when it doesn't guarantee an implementation? Just because there isn't a formal spec, doesn't mean that the underlying systems aren't built with some rules, grounded in computer science and math. We believe that the systems we've set up do guarantee those properties, even if they haven't yet been formally verified. And a subset of them have been formally verified, which also increases confidence. Adding to that confidence level is empirical results: while people have found implementation bugs, which will always exist in any implementation, nobody has managed to demonstrate that the model is fundamentally broken. That it's been years, and many people have tried, also leads us to suspect that our conclusions are correct here. Put another way: not all specs are equal. Some are formal, some are informal. Just having a spec doesn't actually guarantee anything either. Most languages don't have a specification at all.
- chessturk 8y ago
  > Put another way: not all specs are equal. Some are formal, some are informal. So is the argument that the language reference is as good as many existing language specifications, and my complaint is only one of semantics?
  - steveklabnik 8y ago
    Yes, it's basically about what you mean by "guarantee". Very few things are formally guaranteed. People tend to use "guarantee" to mean "I believe this is true with a very high level of confidence."
  - deleted 8y ago
    [deleted]

steveklabnik 8y ago

> How can folk say Rust guarantees safety when it doesn't guarantee an implementation? Just because there isn't a formal spec, doesn't mean that the underlying systems aren't built with some rules, grounded in computer science and math. We believe that the systems we've set up do guarantee those properties, even if they haven't yet been formally verified. And a subset of them have been formally verified, which also increases confidence. Adding to that confidence level is empirical results: while people have found implementation bugs, which will always exist in any implementation, nobody has managed to demonstrate that the model is fundamentally broken. That it's been years, and many people have tried, also leads us to suspect that our conclusions are correct here. Put another way: not all specs are equal. Some are formal, some are informal. Just having a spec doesn't actually guarantee anything either. Most languages don't have a specification at all.

chessturk 8y ago
> Put another way: not all specs are equal. Some are formal, some are informal. So is the argument that the language reference is as good as many existing language specifications, and my complaint is only one of semantics?
- steveklabnik 8y ago
  Yes, it's basically about what you mean by "guarantee". Very few things are formally guaranteed. People tend to use "guarantee" to mean "I believe this is true with a very high level of confidence."
- deleted 8y ago
  [deleted]