Postscript
Looking Back
- Functional programming:
- "declarative" programming style (recursion over persistent data structures, rather than looping over mutable arrays or pointer structures)
- higher-order functions
- polymorphism
- Logic, the mathematical basis for software engineering:
logic calculus -------------------- ~ ---------------------------- software engineering mechanical/civil engineering
- inductively defined sets and relations
- inductive proofs
- proof objects
- Coq, an industrial-strength proof assistant
- functional core language
- core tactics
- automation
- Foundations of programming languages
- notations and definitional techniques for precisely specifying
- abstract syntax
- operational semantics
- big-step style
- small-step style
- type systems
- program equivalence
- Hoare logic
- fundamental metatheory of type systems
- progress and preservation
- progress and preservation
- theory of subtyping
- notations and definitional techniques for precisely specifying
Looking Around
CompCert
CompCert is a fully verified optimizing compiler for almost all of the ISO C_{90} / ANSI C language, generating code for x_{86}, ARM, and PowerPC processors. The whole of CompCert is is written in Gallina and extracted to an efficient OCaml program using Coq's extraction facilities.- The striking thing about our CompCert results is that the middle-end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users.
seL4
seL4 is a fully verified microkernel, considered to be the world's first OS kernel with an end-to-end proof of implementation correctness and security enforcement. It is implemented in C and ARM assembly and specified and verified using Isabelle. The code is available as open source.CertiKOS
CertiKOS is a clean-slate, fully verified hypervisor, written in CompCert C and verified in Coq.Ironclad
Ironclad Apps is a collection of fully verified web applications, including a "notary" for securely signing statements, a password hasher, a multi-user trusted counter, and a differentially-private database.Verdi
Verdi is a framework for implementing and formally verifying distributed systems.DeepSpec
The Science of Deep Specification is an NSF "Expedition" project (running from 2016 to 2020) that focuses on the specification and verification of full functional correctness of both software and hardware. It also sponsors workshops and summer schools.- Website: http://deepspec.org/
- Overview presentations:
REMS
REMS is a european project on Rigorous Engineering of Mainstream Systems. It has produced detailed formal specifications of a wide range of critical real-world interfaces, protocols, and APIs, including the C language, the ELF linker format, the ARM, Power, MIPS, CHERI, and RISC-V instruction sets, the weak memory models of ARM and Power processors, and POSIX filesystems.Others
- Vellvm (formal specification and verification of LLVM optimization passes)
- Zach Tatlock's formally certified browser
- Tobias Nipkow's formalization of most of Java
- The CakeML verified ML compiler
- Greg Morrisett's formal specification of the x_{86} instruction set and the RockSalt Software Fault Isolation tool (a better, faster, more secure version of Google's Native Client)
- Ur/Web, a programming language for verified web applications embedded in Coq
- the Princeton Verified Software Toolchain
Looking Forward
- This book includes several optional chapters covering topics
that you may find useful. Take a look at the table of contents and the chapter dependency diagram to find
them.
- Cutting-edge conferences on programming languages and formal
verification:
- Principles of Programming Langauges (POPL)
- Programming Language Design and Implementation (PLDI)
- SPLASH/OOPSLA
- International Conference on Functional Programming (ICFP)
- Computer Aided Verification (CAV)
- Interactive Theorem Proving (ITP)
- Principles in Practice workshop (PiP)
- CoqPL workshop
- More on functional programming
- Learn You a Haskell for Great Good, by Miran Lipovaca [Lipovaca 2011].
- Real World Haskell, by Bryan O'Sullivan, John Goerzen, and Don Stewart [O'Sullivan 2008]
- ...and many other excellent books on Haskell, OCaml,
Scheme, Racket, Scala, F sharp, etc., etc.
- More on Hoare logic and program verification
- The Formal Semantics of Programming Languages: An Introduction, by Glynn Winskel [Winskel 1993].
- Many practical verification tools, e.g. Microsoft's
Boogie system, Java Extended Static Checking, etc.
- More on the foundations of programming languages:
- Concrete Semantics with Isabelle/HOL, by Tobias Nipkow and Gerwin Klein [Nipkow 2014]
- Types and Programming Languages, by Benjamin C. Pierce [Pierce 2002].
- Practical Foundations for Programming Languages, by Robert Harper [Harper 2016].
- Foundations for Programming Languages, by John
C. Mitchell [Mitchell 1996].
- More on Coq:
- Verified Functional Algorithms, by Andrew Appel [Chlipala 2013].
- Certified Programming with Dependent Types, by Adam Chlipala [Chlipala 2013].
- Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, by Yves Bertot and Pierre Casteran [Bertot 2004].
- Iron Lambda (http://iron.ouroborus.net/) is a collection of Coq formalisations for functional languages of increasing complexity. It fills part of the gap between the end of the Software Foundations course and what appears in current research papers. The collection has at least Progress and Preservation theorems for a number of variants of STLC and the polymorphic lambda-calculus (System F).
(* $Date: 2016-12-08 16:57:10 -0500 (Thu, 08 Dec 2016) $ *)