4 ms·

> The answer isn't generics, Coq, or some fancy type system nobody will understand or use properly. The solution is a formal semantics for unsafe Rust, so that

> The answer isn't generics, Coq, or some fancy type system nobody will understand or use properly. The solution is a formal semantics for unsafe Rust, so that programmers can prove that their unsafe Rust code is safe to use by whatever means they prefer. (Mine would be by hand.) --- Reply to dmix: A formal semantics doesn't have to be particularly fancy, although in Rust's case, it will in most likelihood not be straightforward either.

dmix 9y ago
Is that a fancy <x> system that nobody will understand or use properly? (Honest question)
- steveklabnik 9y ago
  We intend for it not to be; more on that as we get closer to actually having a model.
- Animats 9y ago
  Probably. I used to do formal proof of correctness work and headed a project to build a verifier.[1] That stuff is very hard. The partially initialized array thing is an issue of expressive power. You can't talk about that in Rust yet. This is a classic issue. The three big headaches in C around memory safety are "how big is it", "who owns it", and "who locks it". The language lacks the syntax to even talk about those issues. Rust can talk about those, which is a huge step forward. Before you can even consider verifying something, you have to be able to talk about it in some formal language. Preferably the one you're programming in. Having to do formal specifications in a separate language is a huge headache. Been there, done that. There are a few standard trouble spots. I've listed two of them. Most other unsafe code comes from 1) Foreign functions, which can be expected to decline over time as more libraries are implemented in Rust. (How's SSL/TLS in Rust coming along?) 2) "Optimization", which may be premature. This usually consists of bypassing subscript checks. I'd rather have the subscript checks on all the time, and see effort put into hoisting subscript checks out inner loops. (Subscript checks that aren't in inner loops usually aren't significant overhead items.) 3) replicating C/C++ code in Rust. (An early attempt was a transliteration of Doom into Rust, with lots of pointer arithmetic.) Remember, it can blow at any seam. It only takes one buffer overflow to allow an exploit. [1] https://github.com/John-Nagle/pasv https://github.com/John-Nagle/pasv
  - dmix 9y ago
    > Before you can even consider verifying something, you have to be able to talk about it in some formal language. Preferably the one you're programming in. I'd personally be excited too see a modern language implement this. I saw the potential for this type of verification in my (hobbyist) dabbling with Haskell. Which subsequently inspired me to relearn math, including a great book on proofs recommended on HN which really changed the way I viewed/approached math. The use-case analogies for formal verification can probably best be drawn from automated testing and TDD. Which is another 'optional' part of programming with varying degrees of usage - although with a lower barrier to entry. Types/proofs seem to have a positive influence on the 'best practice' part as well, as it promotes a programming style which force you to really consider the implementations you're coding. Very similar to testing. At the moment formal proofs tools today seems to me like a rabbit hole with questionable practical ROI so I've been hesitant to try out the current state-of-the-art. Assuming it does get built in to the language, even if it doesn't get used by the user they will likely benefit just by being able to build on layers beneath that were proven in the standard/popular libraries. I felt a similar feeling of assurance when building on top of well-typed Haskell libraries.
    - Animats 9y ago
      We built verification into the language in Pascal-F, 30 years ago.[1] That's rarely been done since in real-world imperative languages. It's much easier to keep the verification statements correct if they're in the same file and the same language as the program. But Pascal was a small language. Getting this into today's bloated languages is tough. Back then, we looked at Ada, sized the project, and realized it was comparable to building an optimizing compiler for the language. [1] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf
      - dmix 9y ago
        > We built verification into the language in Pascal-F, 30 years ago. You sound like a very interesting person to buy a beer for, assuming you'd be patient enough for my questions :p, I'll check out the paper instead when I get the time. > It's much easier to keep the verification statements correct if they're in the same file and the same language as the program. Agreed. Hell even using Dialyzer in Erlang/Elixir for static type checking (which I make the effort to do often in my daily side project hacking) just doesn't feel right, even though it's still appended to function definitions in the original files. This is one of those things that need to be a core part of the language design IMO, not just a tool built on top - 3rd party, by the core team, or otherwise. But, that said, tooling can still be superior compared to the complete absence of it. Maybe you can answer a question I've been struggling to find the answer to via Google. Do you know the name of this popular older language/tool used by to Microsoft for doing formal verification? For c/c++ style code. It sounds like tkk or something similar? I can't seem to find it. My other question I'd ask is if you think the testing analogy applies here as I mentioned in my comment above or do you see it as an entirely different paradigm? Basically changing how you program rather than adding on a tool/skillset.
steveklabnik 9y ago
This is being worked on! Several bits of the rust standard library have already been proven safe in the initial model.
hashmal 9y ago
In the meantime, Rust's support for automated tests is great.
- catnaroek 9y ago
  Alas, tests aren't proofs.
  - burntsushi 9y ago
    Yet, tests are still useful!
    - catnaroek 9y ago
      Not if the goal is to prove that an algorithm meets a specification, which is more often than not my goal.

dmix 9y ago

Is that a fancy <x> system that nobody will understand or use properly? (Honest question)

steveklabnik 9y ago
We intend for it not to be; more on that as we get closer to actually having a model.
Animats 9y ago
Probably. I used to do formal proof of correctness work and headed a project to build a verifier.[1] That stuff is very hard. The partially initialized array thing is an issue of expressive power. You can't talk about that in Rust yet. This is a classic issue. The three big headaches in C around memory safety are "how big is it", "who owns it", and "who locks it". The language lacks the syntax to even talk about those issues. Rust can talk about those, which is a huge step forward. Before you can even consider verifying something, you have to be able to talk about it in some formal language. Preferably the one you're programming in. Having to do formal specifications in a separate language is a huge headache. Been there, done that. There are a few standard trouble spots. I've listed two of them. Most other unsafe code comes from 1) Foreign functions, which can be expected to decline over time as more libraries are implemented in Rust. (How's SSL/TLS in Rust coming along?) 2) "Optimization", which may be premature. This usually consists of bypassing subscript checks. I'd rather have the subscript checks on all the time, and see effort put into hoisting subscript checks out inner loops. (Subscript checks that aren't in inner loops usually aren't significant overhead items.) 3) replicating C/C++ code in Rust. (An early attempt was a transliteration of Doom into Rust, with lots of pointer arithmetic.) Remember, it can blow at any seam. It only takes one buffer overflow to allow an exploit. [1] https://github.com/John-Nagle/pasv https://github.com/John-Nagle/pasv
- dmix 9y ago
  > Before you can even consider verifying something, you have to be able to talk about it in some formal language. Preferably the one you're programming in. I'd personally be excited too see a modern language implement this. I saw the potential for this type of verification in my (hobbyist) dabbling with Haskell. Which subsequently inspired me to relearn math, including a great book on proofs recommended on HN which really changed the way I viewed/approached math. The use-case analogies for formal verification can probably best be drawn from automated testing and TDD. Which is another 'optional' part of programming with varying degrees of usage - although with a lower barrier to entry. Types/proofs seem to have a positive influence on the 'best practice' part as well, as it promotes a programming style which force you to really consider the implementations you're coding. Very similar to testing. At the moment formal proofs tools today seems to me like a rabbit hole with questionable practical ROI so I've been hesitant to try out the current state-of-the-art. Assuming it does get built in to the language, even if it doesn't get used by the user they will likely benefit just by being able to build on layers beneath that were proven in the standard/popular libraries. I felt a similar feeling of assurance when building on top of well-typed Haskell libraries.
  - Animats 9y ago
    We built verification into the language in Pascal-F, 30 years ago.[1] That's rarely been done since in real-world imperative languages. It's much easier to keep the verification statements correct if they're in the same file and the same language as the program. But Pascal was a small language. Getting this into today's bloated languages is tough. Back then, we looked at Ada, sized the project, and realized it was comparable to building an optimizing compiler for the language. [1] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf
    - dmix 9y ago
      > We built verification into the language in Pascal-F, 30 years ago. You sound like a very interesting person to buy a beer for, assuming you'd be patient enough for my questions :p, I'll check out the paper instead when I get the time. > It's much easier to keep the verification statements correct if they're in the same file and the same language as the program. Agreed. Hell even using Dialyzer in Erlang/Elixir for static type checking (which I make the effort to do often in my daily side project hacking) just doesn't feel right, even though it's still appended to function definitions in the original files. This is one of those things that need to be a core part of the language design IMO, not just a tool built on top - 3rd party, by the core team, or otherwise. But, that said, tooling can still be superior compared to the complete absence of it. Maybe you can answer a question I've been struggling to find the answer to via Google. Do you know the name of this popular older language/tool used by to Microsoft for doing formal verification? For c/c++ style code. It sounds like tkk or something similar? I can't seem to find it. My other question I'd ask is if you think the testing analogy applies here as I mentioned in my comment above or do you see it as an entirely different paradigm? Basically changing how you program rather than adding on a tool/skillset.

steveklabnik 9y ago

This is being worked on! Several bits of the rust standard library have already been proven safe in the initial model.

hashmal 9y ago

In the meantime, Rust's support for automated tests is great.

catnaroek 9y ago
Alas, tests aren't proofs.
- burntsushi 9y ago
  Yet, tests are still useful!
  - catnaroek 9y ago
    Not if the goal is to prove that an algorithm meets a specification, which is more often than not my goal.