Viktor Kuncak (EPFL): Propositions as Programs, Proofs as Programs
Leon is a system that (among other features) enables writing verified programs and their properties in a purely functional subset of Scala. The key specification statement in Leon is that a function satisfies its contract for all inputs. Leon proves properties and finds counterexamples using SMT solvers and an unfolding strategy for recursive functions. A newly developed link with Isabelle provides additional safety net for soundness of the approach.
Due to Leon’s unfolding mechanism, it is possible to write additional, semantically redundant, expressions that help Leon prove a theorem. We attempt to formalize this “accidental” feature of Leon. In our view, propositions, as well as proofs, are just terminating programs. This makes Leon statements and proofs (syntactically) accessible to the half a million of Scala developers. We explain some limitations of this approach in writing proof tactics and controlling the space of assumptions, suggesting that a form of reflection would provide benefits of Turing-complete tactic language without ever leaving the paradise of purely functional Scala programs.
Grant Olney Passmore (Aesthetic Integration and University of Cambridge): Formal Verification of Financial Algorithms, Progress and Prospects
Many deep issues plaguing today’s financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. At Aesthetic Integration, we’ve pioneered the use of formal verification for analysing the safety and fairness of financial algorithms. With a focus on financial infrastructure (e.g., the matching logics of exchanges and dark pools), we’ll describe the landscape, and illustrate our Imandra formal verification system on a number of real-world examples. We’ll sketch many open problems and future directions along the way.
Nikhil Swamy (Microsoft Research): Dijkstra monads for free: A framework for deriving and extending F*’s effectful semantics
F* is a higher-order effectful language with dependent types. It aims to provide equal support for general purpose programming (as in the ML family of languages) as well as for developing formal proofs (like other type-theory based proof assistants, e.g., Coq, Agda or Lean). By making use of an SMT solver while type-checking, F* provides automation for many routine proofs.
At the heart of F* is the manner in which effects and dependent types are combined. This presents several well-known difficulties. Our basic approach to solving these difficulties is not surprising: effectful computations are encapsulated within monad-like structures. More specifically, F* interprets effectful computations using monads of predicate transformers, so called “Dijkstra monads” that compute weakest pre-conditions for arbitrary post-conditions. These Dijkstra monads are arranged in a lattice of effect inclusions, e.g., pure computations are included within stateful ones.
In this talk, I will describe a new technique for deriving F*’s Dijkstra monad lattice by CPS’ing (with result type Prop) purely functional definitions of monads corresponding to F*’s effects. Several benefits ensue:
- For starters, programmers are able to customize F*’s effect lattice using familiar Haskell-style monadic definitions, while gaining for each such monad a weakest pre-condition calculus suitable for Hoare-style verification of programs.
- Next, several useful properties, e.g., monotonicity of predicate transformers, are guaranteed by the derivation, reducing the proof obligations for adding an effect to F*.
- Third, our technique supports a mechanism to break the abstraction of a monadic effect in a controlled manner, reifying an effectful computation as its pure counterpart, and reflecting pure reasoning on the reified program back on to the effectful code.
I will also provide a general introduction to F* and its applications, notably its use in Everest, a new project to build and deploy a verified, secure implementation of HTTPS, including Transport Layer Security, TLS-1.3.
F* is open source and developed on github by researchers at Microsoft Research and Inria. For more information, visit https://fstar-lang.org.
