Get some feedback on current direction of impl

[Apolexian]

No description provided.

[Apolexian]

The general idea of what I have done:

• Make all TCP messages into types
• Create session type actions (Send, Recv, Choose, Branch, etc) as types that operate on these messages

This means that I can write something like:

type Example = Offer<Send<Segment, Terminate>, Recv<Abort, Terminate>>;

and

type ExampleDual = <Offer<Send<Segment, Terminate>, Recv<Abort, Terminate>> as Action>::Dual;

Each action also has a Cont type that indicates the continuation after the action. Hence, I should be able to enforce communication at a type level via send and receive functions.

For example (not actually working code):

fn send(m: Message, s: Action) -> Action {
    s.do_send();
    return s::Cont;
}

This means that the next send or recv would use the continuation action, so if we get an unexpected message it will not type check.

Which looks quite similar to session type syntax and can encode a protocol in types.

Things I do not yet know/understand how to do:

1. Seems like we will need recursive session types? I.e. currently we explicitly state the End of communication deterministically, which is obviously impossible with a network protocol. So we need a mechanism that says that we can arbitrarily do a sequence of receiving/sending/etc.

2. Branches need labels and we need to be able to offer/choose on these labels. These also have to be type checked. Annoyingly, Rust does not have variadic generics - Draft RFC: variadic generics rust-lang/rfcs#376 (and C++ has a host of other issues), so my Offer and Choose construct can only do so between two choices. You can probably encode a variable number of choices using two by recursing, so need to look for a paper that does this.

3. From a usability perspective is that this does not explicitly show "state" as we have state in RFCs.
   The state of the protocol is rather determined by the sequence of messages and continuations we can take.
   From a usability perspective it may be worth either: seeing if there is some ST system that can do explicit "labels" (not in the meaning of branching labels but rather something like type SillyServer = <(Closed, Ended), Recv<Segment, Send<Abort, End>>>; , i.e. to transition from closed to ended we use the following communication.
   Or perhaps <Closed, Recv<Segment, <Ended, Send<Abort, End>>>
   I'm not sure how this would work, but the semantics are not terribly important.

4. To do the static portion we can probably use thread channels to simulate network connections and make sure the protocol state machine makes sense.
   On the network, we will have to do runtime verification to see if an incoming packet is of the correct type. So, we can get a packet, extract the message type, verify that this message type makes sense, and if not, abort (or whatever else needs to happen).

[Apolexian]

Should make sure to look at TCP RFC to see if states and transitions are correct.

Might be good to consider minimal impl (e.g. try just model handshake)

It is good to have well defined failure states.