3 ms·

I'd hoped that rust would have a lot of powerful tools for typing and exposing invariants and contracts— tools to help create provably reliable software. As sex

by nullc 14y ago

I'd hoped that rust would have a lot of powerful tools for typing and exposing invariants and contracts— tools to help create provably reliable software. As sexy as new programming tools are, the big problem in software today is that we simply can't manage the complexity of it and as a result _everything_ is full of bugs and unintended behavior. Addon layers like ACSL are hard to use and messy because they work at odds with the language, instead, e.g. of being integrated with the typesystem. I was hopeful that rust could really advance the art here in the context of practically usable systems (vs academic toys) and I suppose it does, but it also lost features for formal analysis between versions and as its now becoming stable I suppose they won't return.

pcwalton 14y ago
I assume you're referring to typestate. One of the reasons that typestate was removed is that practically everything you can do with typestate can be done with session types instead. Constraints can be modeled as unique types with a trusted transition function from state to state. The unique type system used for memory management in Rust nicely doubles as a session type system. This is actually done today with the pipes compiler—it uses unique types to statically ensure that you can't violate a communications protocol, just as typestate can. One of our focuses for 1.0 is on aggressively pruning features that overlap, to reduce language complexity and to avoid committing ourselves to language features we might not need. However, future versions of the language might add more static analyses as they prove useful.
- doublec 14y ago
  Do you have any code examples of where this is used that I can look at? Like nullc my interest is in the area of types being used to enforce contracts and safetly (hence my interest in the ATS language). Typesafe was my initial interest in Rust and I'd love to see examples of how this is being approached in Rust as it is now.
  - pcwalton 14y ago
    Probably the best place to look at the moment is this presentation: https://air.mozilla.org/intern-presentation-message-passing-in-rust/ https://air.mozilla.org/intern-presentation-message-passing-...
    - nullc 14y ago
      Perhaps I missed where it was explained— but I don't see how rust enforces the type predicates (e.g. acquire vs wait state) there without typestate.
      - pcwalton 14y ago
        Say I have a protocol that transitions from A -> B -> C. Since the pipes compiler creates the only constructor for type B, there's no way for you to construct a value of type B (in the safe language) without giving up your one value of type A. The uniqueness typing system prevents you from copying your single value of A, and you must surrender all your references to it at the time you transition to state B.

by nullc 14y ago

pcwalton 14y ago

I assume you're referring to typestate. One of the reasons that typestate was removed is that practically everything you can do with typestate can be done with session types instead. Constraints can be modeled as unique types with a trusted transition function from state to state. The unique type system used for memory management in Rust nicely doubles as a session type system. This is actually done today with the pipes compiler—it uses unique types to statically ensure that you can't violate a communications protocol, just as typestate can. One of our focuses for 1.0 is on aggressively pruning features that overlap, to reduce language complexity and to avoid committing ourselves to language features we might not need. However, future versions of the language might add more static analyses as they prove useful.

doublec 14y ago
Do you have any code examples of where this is used that I can look at? Like nullc my interest is in the area of types being used to enforce contracts and safetly (hence my interest in the ATS language). Typesafe was my initial interest in Rust and I'd love to see examples of how this is being approached in Rust as it is now.
- pcwalton 14y ago
  Probably the best place to look at the moment is this presentation: https://air.mozilla.org/intern-presentation-message-passing-in-rust/ https://air.mozilla.org/intern-presentation-message-passing-...
  - nullc 14y ago
    Perhaps I missed where it was explained— but I don't see how rust enforces the type predicates (e.g. acquire vs wait state) there without typestate.
    - pcwalton 14y ago
      Say I have a protocol that transitions from A -> B -> C. Since the pipes compiler creates the only constructor for type B, there's no way for you to construct a value of type B (in the safe language) without giving up your one value of type A. The uniqueness typing system prevents you from copying your single value of A, and you must surrender all your references to it at the time you transition to state B.