Secure Distributed Programming With Value-Dependent Types
Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications, and proofs becomes challenging. Although these languages are successful in many aspects, for large-scale distributed programming, the authors desire languages that feature general programming constructs like effects and recursion, which, while invaluable for building real systems, make it hard to formally reason about programs, specifications, and proofs; support various styles of proofs and evidence, ranging from cryptographic signatures to logical proof terms; produce proofs that can be efficiently communicated between agents in the system.