4 ms·

I’m not sure if I’m misunderstanding the purpose of session-types, but it seem that this a lot like finagle but for rust? Session type is basically just a fina

I’m not sure if I’m misunderstanding the purpose of session-types, but it seem that this a lot like finagle but for rust? Session type is basically just a finagle service, etc... Or are they more like go channels?

steveklabnik 8y ago
Session types are more like “encode a state machine in your type system so it’s impossible to mess it up”. They don’t inherently have to do with network services, though since network services follow protocols that can be represented as state machines (think “the S in REST”), they’re a good application of session types. That said, it looks like this library is not purely about session types, but applying them to channels. (Which are go-style, yes.)
- agumonkey 8y ago
  are they used in non academic contexts ?
  - Munksgaard 8y ago
    I'm one of the authors of the original paper/repository. Part of the motivation behind our work was to try and apply it to the Servo project (Mozilla's experimental browser engine, of which parts have already been integrated into Firefox), which is highly parallelized. They had issues with their internal communication because of their expansive use of threads, and we wanted to see if session types could be applied to fix that. Unfortunately, Servo is a rapidly moving target, so while we did manage to convert some parts of the project to use our session types library, we never got around to finishing the work, and now I believe that they've found different solutions to their challenges. With regards to your first question, this library is solely for in-process communication. The concept could be expanded to cover inter-process communication as well as communication over the network, and actually has been in other similar session type projects, but focusing on in-process communication allows us to make stronger guarantees.
    - agumonkey 8y ago
      Very nice
paulddraper 8y ago
Session types are essentially a type-checked FSM. So if your type checker passes, your FSM obeys the protocol requirements. (Namely, it does not pass between states in an illegal manner.)
- cwillu 8y ago
  This sounds a lot like the invariant that they're checking is that, _given a conforming counter-party_, nothing illegal will happen. But this doesn't tell you anything about what happens to you when your peer passes between states in an illegal manner. I'd expect this to have been emphasised in the paper. Especially if their threat model includes it, it would be a key selling point.

steveklabnik 8y ago

Session types are more like “encode a state machine in your type system so it’s impossible to mess it up”. They don’t inherently have to do with network services, though since network services follow protocols that can be represented as state machines (think “the S in REST”), they’re a good application of session types. That said, it looks like this library is not purely about session types, but applying them to channels. (Which are go-style, yes.)

agumonkey 8y ago
are they used in non academic contexts ?
- Munksgaard 8y ago
  I'm one of the authors of the original paper/repository. Part of the motivation behind our work was to try and apply it to the Servo project (Mozilla's experimental browser engine, of which parts have already been integrated into Firefox), which is highly parallelized. They had issues with their internal communication because of their expansive use of threads, and we wanted to see if session types could be applied to fix that. Unfortunately, Servo is a rapidly moving target, so while we did manage to convert some parts of the project to use our session types library, we never got around to finishing the work, and now I believe that they've found different solutions to their challenges. With regards to your first question, this library is solely for in-process communication. The concept could be expanded to cover inter-process communication as well as communication over the network, and actually has been in other similar session type projects, but focusing on in-process communication allows us to make stronger guarantees.
  - agumonkey 8y ago
    Very nice

paulddraper 8y ago

Session types are essentially a type-checked FSM. So if your type checker passes, your FSM obeys the protocol requirements. (Namely, it does not pass between states in an illegal manner.)

cwillu 8y ago
This sounds a lot like the invariant that they're checking is that, _given a conforming counter-party_, nothing illegal will happen. But this doesn't tell you anything about what happens to you when your peer passes between states in an illegal manner. I'd expect this to have been emphasised in the paper. Especially if their threat model includes it, it would be a key selling point.