세션 타입은 작동한다. 대부분의 언어가 단지 구현을 거부했을 뿐이다.
세션 타입은 통신 프로토콜을 타입 시스템에 인코딩하여 런타임 프로토콜 오류를 컴파일 시간 오류로 변환한다. 프로덕션 코드가 사용할 수 있게 되기까지 연구 논문에서 30년을 보낸 이유는 다음과 같다.
세션 타입은 1993년에 발명되었다. 30년 후, 대부분의 네트워크 서비스는 여전히 프로토콜 상태를 수작업으로 작성한 런타임 검사로 검증하고 있다. 애초에 검증하는지조차 미지수다. 타입 시스템은 클라이언트가 전에 을 보냈는지, 또는 누군가 닫는 것을 잊어 연결이 누출되었는지에 대해…