Verified Networking using Dependent Types by Simon Fowler.
Abstract:
Strongly, statically typed functional programming languages have found a strong grounding in academia and industry for a variety of reasons: they are concise, their type systems provide additional static correctness guarantees, and the structured management of side effects aids easier reasoning about the operation of programs, to name but a few.
Dependently-typed languages take these concepts a step further: by allowing types to be predicated on values, it is possible to impose arbitrarily specific type constraints on functions, resulting in increased confidence about their runtime behaviour.
This work demonstrates how dependent types may be used to increase confidence in network applications. We show how dependent types may be used to enforce resource usage protocols inherent in C socket programming, providing safety guarantees, and examine how a dependently- typed embedded domain-specific language may be used to enforce the conformance of packets to a given structure. These concepts are explored using two larger case studies: packets within the Domain Name System (DNS) and a networked game.
The use of statically typed functional programming languages is spreading. Fowler’s dissertation is yet another illustration of that fact.
When you read:
…examine how a dependently- typed embedded domain-specific language may be used to enforce the conformance of packets to a given structure.
Do you also hear:
…examine how a dependently- typed embedded domain-specific language may be used to enforce the conformance of proxies to a given structure.
??