  Session types are a typing discipline used to formally describe
communication-driven applications with the aim of fewer errors and easier
debugging later into the life cycle of the software. Protocols at the transport
layer such as TCP, UDP, and QUIC underpin most of the communication on the
modern Internet and affect billions of end-users. The transport layer has
different requirements and constraints compared to the application layer
resulting in different requirements for verification. Despite this, to our best
knowledge, no work shows the application of session types at the transport
layer. In this work, we discuss how multiparty session types (MPST) can be
applied to implement the TCP protocol. We develop an MPST-based implementation
of a subset of a TCP server in Rust and test its interoperability against the
Linux TCP stack. Our results highlight the differences in assumptions between
session type theory and the way transport layer protocols are usually
implemented. This work is the first step towards bringing session types into
the transport layer.
