nLab certified programming

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

General

A certification or formal verification of a computer program is a formalized guarantee – a proof – that the program has given specified properties. For instance, it could be guaranteed to compute a given output based on a given input, or to always terminate, or to not include a certain kind of security hole.

Certifications often take the form of a formal proof (whence “formal methods” WLBF09) that a program, regarded as a term of some sort (under programs as proofs), has a specified type. Thus, programming languages based on highly expressive type theories (including dependent types) are a natural place to do certified programming “natively”. Examples are Coq and Agda. In this case, the program is written at the same time as a proof of its certification. One often then wants to “extract” the executable code or “ignore” the proof part of the terms when actually running the code, for performance reasons; Coq and Agda include mechanisms designed for this.

It is also possible to write a program in some less strongly typed language and provide an “external” certification for it, rather than one built into the program itself. Computer proof assistants like Coq and Agda are also used for this, using a formal representation of some other programming language. There are also other program analysis tools which can produce automated proofs of certain aspects of a computer program, such as safety and termination (although of course a complete solution to termination-checking is impossible, being the halting problem).

Via homotopy type theory

From Ghani et al. 15:

The cost of software failure is truly staggering. Well known individual cases include the Mars Climate Orbiter failure (£80 million), Ariane Rocket disaster (£350 million), Pentium Chip Division failure (£300 million), and more recently the heartbleed bug (est. £400 million). There are many, many more examples. Even worse, failures such as one in the Patriot Missile System and another in the Therac-25 radiation system have cost lives. More generally, a 2008 study by the US government estimated that faulty software costs the US economy £100 billion annually.

There are many successful approaches to software verification (testing, model checking etc). One approach is to find mathematical proofs that guarantees of software correctness. However, the complexity of modern software means that hand-written mathematical proofs can be untrustworthy and this has led to a growing desire for computer-checked proofs of software correctness. Programming languages and interactive proof systems like Coq, Agda, NuPRL and Idris have been developed based on a formal system called Martin-Löf type theory. In these systems, we can not only write programs, but we can also express properties of programs using types, and write programs to express proofs that our programs are correct.

In this way, both large mathematical theorems such as the Four Colour Theorem, and large software systems such as the CompCert C compiler have been formally verified. However, in such large projects, the issue of scalability arises: how can we use these systems to build large libraries of verified software in an effective way?

This is related to the problem of reusability and modularity: a component in a software system should be replaceable by another which behaves the same way even though it may be constructed in a completely different way. That is, we need an “extensional equality” which is computationally well behaved (that is, we want to run programs using this equality). Finding such an equality is a fundamental and difficult problem which has remained unresolved for over 40 years.

But now it looks like we might have a solution! Fields medalist Vladimir Voevodsky has come up with a completely different take on the problem by thinking of equalities as paths such as those which occur in one of the most abstract branches of mathematics, namely homotopy theory, leading to Homotopy Type Theory (HoTT). In HoTT, two objects are completely interchangeable if they behave the same way. However, most presentations of HoTT involve axioms which lack computational justification and, as a result, we do not have programming languages or verification systems based upon HoTT. The goal of our project is to fix that, thereby develop the first of a new breed of HoTT-based programming languages and verification systems, and develop case studies which demonstrate the power of HoTT to programmers and those interested in formal verification.

Examples

(…)

References

General

Introduction:

  • Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, John Fitzgerald, Formal methods: Practice and experience, ACM Computing Surveys 41 19 (2009) 1–36 [doi:10.1145/1592434.1592436]

  • Patrick Cousot, Radhia Cousot, A gentle introduction to formal verification of computer systems by abstract interpretation, NATO Science for Peace and Security Series - D: Information and Communication Security, 25 Logics and Languages for Reliability and Security (2009)[doi:10.3233/978-1-60750-100-8-1, pdf, pdf]

  • John Harrison, Formal Verification, Lecture notes Marktoberdorf 2010 [web, pdf, pdf]

  • Catherine Meadows, Program Verification and Security (doi:10.1007/978-1-4419-5906-5_863), In: Henk C. A. van Tilborg, Sushil Jajodia (ed.) Encyclopedia of Cryptography and Security Springer (2011)

  • Bas Spitters, Robberts Krebbers, Eelis van der Weegen, From computational analysis to thoughts about analysis in HoTT, MAP International spring school on formalization of Mathematics (2012) (pdf)

See also:

Sources listing real-world issues programming issues that might motivate verification of software include

For cryptography

Software verification for cryptography:

Verification of cryptography via type theory:

  • Cédric Fournet, Karthikeyan Bhargavan, Andrew D. Gordon, Cryptographic Verification by Typing for a Sample Protocol Implementation, In: Aldini A., Gorrieri R. (eds) Foundations of Security Analysis and Design VI. FOSAD 2011. Lecture Notes in Computer Science, vol 6858. Springer (2011) (doi:10.1007/978-3-642-23082-0_3)

  • Cédric Fournet, Markulf Kohlweiss, Pierre-Yves Strub, Modular code-based cryptographic verification, CCS ‘11: Proceedings of the 18th ACM conference on Computer and communications securityOctober 2011 Pages 341–350 (doi:10.1145/2046707.2046746)

Via Hoare calculus

Program verification via Hoare calculus:

For quantum programming languages:

Via (dependent) type theory

The general idea of verified programming via dependent type theory:

Exposition:

Software verification via dependent type theory (such as in Coq or Agda):

On Agda as a dependently typed certification language:

  • Aaron Stump, Verified Functional Programming in Agda, Association for Computing Machinery and Morgan & Claypool (2016) [doi:10.1145/2841316, ISBN:978-1-970001-27-3]

Application to consensus algorithms

Verification of (blockchain-like) hashgraph consensus algorithms:

Background:

  • Pierre Tholoniat, Vincent Gramoli, Formal Verification of Blockchain Byzantine Fault Tolerance, in Handbook on Blockchain, Optimization and Its Applications 194, Springer (2022) [arXiv:1909.07453, doi:10.1007/978-3-031-07535-3_12]

  • Leemon Baird, Mance Harmon, and Paul Madsen, Hedera: A Public Hashgraph Network & Governing Council, (last update 2020) [pdf]

With Coq:

With Agda:

  • Harold Carr, Christopher Jenkins, Mark Moir, Victor Cacciari Miraldo, Lisandra Silva, Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version, in: NASA Formal Methods: 14th International Symposium, NFM 2022 Proceedings (2022) 616–635 [doi:10.1007/978-3-031-06773-0_33, arXiv:2203.14711]

See also:

Via homotopy type theory

Proposals for verification specifically via homotopy type theory:

and here again specifically for cryptography:

Explicitly using type equivalences:

For quantum programming languages

First, on the problem of debugging quantum programs, as maybe first highlighted by VRSAS 2015, Rand (2018) and Ying & Feng (2018):

  • Benoît Valiron, Neil J. Ross, Peter Selinger, D. Scott Alexander, Jonathan M. Smith, Programming the quantum future, Communications of the ACM 58 8 (2015) 52–61 [doi:10.1145/2699415, pdf, web, promo vid:YT]

    [p 6:] “In quantum computation, the cost of debugging is likely to be quite high. To begin with, observing a quantum system can change its state. A debugger for a quantum program would therefore necessarily give incomplete information about its state when run on actual quantum hardware. The alternative is to use a quantum simulator for debugging. But this is not practical due to the exponential cost of simulating quantum systems. Moreover, it can be expected that the initial quantum computers will be rare and expensive to run and therefore that the cost of runtime errors in quantum code will initially be much higher than in classical computing. This shifts the cost-benefit analysis for quantum programming toward strong compile-time correctness guarantees, as well as formal specification and verification.”

    (with an eye towards Quipper)

  • Andriy Miranskyy, Lei Zhang, Javad Doliskani, Is Your Quantum Program Bug-Free?, in ICSE-NIER ‘20: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: New Ideas and Emerging Results (2020) 29–32 [arXiv:2001.10870, doi:10.1145/3377816.3381731]

    “The classical parts of a quantum program can be debugged using traditional methods. The quantum parts, however, can not be treated in the same way because of the properties of a QC – such as superposition, entanglement, and no-cloning – which are governed by the laws of quantum mechanics. The purpose of debugging a program is to present the user with human readable, i.e., classical, information about the runtime state of the system. Extracting classical information from a quantum state is done using measurement which is usually a non-unitary operation and results in collapse of the state, and hence an unintended behavior of the program.”

On formal verification of quantum computing with/of quantum programming languages:

general:

  • Mingsheng Ying, Yuan Feng, Model Checking Quantum Systems — A Survey [arXiv:1807.09466]

    “But to check whether a quantum system satisfies a certain property at a time point, one has to perform a quantum-measurement on the system, which can change the state of the system. This makes studies of the long-term behaviours of quantum systems much harder than that of classical system.”

    “The state spaces of the classical systems that model-checking algorithms can be applied to are usually finite or countably infinite. However, the state spaces of quantum systems are inherently continuous even when they are finite-dimensional. In order to develop algorithms for model-checking quantum systems, we have to exploit some deep mathematical properties of the systems so that it suffices to examine only a finite number of (or at most countably infinitely many) representative elements, e.g. those in an orthonormal basis, of their state spaces.”

(repeated in Ying & Feng (2021, Sec. 1.3))

  • Ji Guan, Yuan Feng, Andrea Turrini, Mingsheng Ying, Model Checking Applied to Quantum Physics [arXiv:1902.03218]

  • Mingsheng Ying, Yuan Feng, Model Checking Quantum Systems – Principles and Algorithms, Cambridge University Press (2021) [ISBN:9781108484305]

  • Christophe Chareton, Sébastien Bardin, Dongho Lee, Benoît Valiron, Renaud Vilmart, Zhaowei Xu, Formal Methods for Quantum Programs: A Survey, in: Handbook of Formal Analysis and Verification in Cryptography, CRC (2023) [arXiv:2109.06493, doi:10.1201/9781003090052]

  • Marco Lewis, Sadegh Soudjani, Paolo Zuliani, Formal Verification of Quantum Programs: Theory, Tools and Challenges [arXiv:2110.01320]

    “Verifying programs is especially important in the quantum setting due to how difficult it is to program complex algorithms correctly on resource-constrained and error-prone quantum hardware.”

  • Carmelo R. Cartiere, Formal Methods for Quantum Software Engineering, in: Quantum Software Engineering, Springer (2022) [doi:10.1007/978-3-031-05324-5_5]

    “The characteristic difficulty in creating pure quantum software is mainly due to the inaccessibility to intermediate states, which makes debugging practically impossible. However, the use of formal methods, which apply rigorous mathematical models to ensure error-free software, can overcome this barrier and enable the production of reliable quantum algorithms and applications right out of the box.”

with QML:

with QPMC:

  • Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, Lijun Zhang, QPMC: A Model Checker for Quantum Programs and Protocols, in Formal Methods. FM 2015, Lecture Notes in Computer Science 9109, Springer (2015) [doi:10.1007/978-3-319-19249-9_17]

    “In practice, however, security analysis of quantum cryptographic protocols is notoriously difficult; for example, the manual proof of BB84 in [15] contains about 50 pages. It is hard to imagine such an analysis being carried out for more sophisticated quantum protocols. Thus, techniques for automated or semi-automated verification of these protocols will be indispensable.”

for Quipper with QPMC:

  • Linda Anticoli, Carla Piazza, Leonardo Taglialegne, Paolo Zuliani, Towards Quantum Programs Verification: From Quipper Circuits to QPMC, In: Devitt S., Lanese I. (eds.) Reversible Computation. RC 2016, Lecture Notes in Computer Science 9720 Springer (2016) [arXiv:1708.06312, doi:10.1007/978-3-319-40578-0_16]

with QWIRE (in Coq):

  • Robert Rand, Jennifer Paykin, Steve Zdancewic, QWIRE Practice: Formal Verification of Quantum Circuits in Coq, EPTCS 266, 2018, pp. 119-132 (arXiv:1803.00699)

  • Robert Rand, Formally Verified Quantum Programming, UPenn (2018) [ediss:3175]

    [p. iv:] “We argue that quantum programs demand machine-checkable proofs of correctness. We justify this on the basis of the complexity of programs manipulating quantum states, the expense of running quantum programs, and the inapplicability of traditional debugging techniques to programs whose states cannot be examined.”

    [p. 3:] “Quantum programs are tremendously difficult to understand and implement, almost guaranteeing that they will have bugs. And traditional approaches to debugging will not help us: We cannot set breakpoints and look at our qubits without collapsing the quantum state. Even techniques like unit tests and random testing will be impossible to run on classical machines and too expensive to run on quantum computers – and failed tests are unlikely to be informative”

    [p. 4:] “Thesis Statement: Quantum programming is not only amenable to formal verification: it demands it.

    “The overarching goal of this thesis is to write and verify quantum programs together. Towards that end, we introduce a quantum programming language called Qwire and embed it inside the Coq proof assistant. We give it a linear type system to ensure that it obeys the laws of quantum mechanics and a denotational semantics to prove that programs behave as desired.”

Further development SQIR:

See also:

Via Hoare logic:

  • Xiaodi Wu, Toward Automatic Verification of Quantum Programs (2019) [pdf]

Projects:

See also

Hardware verification

  • J. Pau Roth, Hardware Verification, IEEE Transactions on Computers C 26 12 (1977) [doi:10.1109/TC.1977.1674795]

  • Paolo Camurati, Paolo Prinetto, Formal Verification of Hardware Correctness: Introductions and Survey of Current Research, ComputerVolume 21 7 (1988) [doi:10.1109/2.65, Computer-doi:10.1109/2.65, pdf]

  • Aarti Gupta, Formal Hardware Verification Methods: A survey, Formal Methods in System Design 1 (1992) 151-238 [doi:10.1007/BF00121125, pdf]

  • Sharad Malik, Hardware Verification: Techniques, Methodology and Solutions, in Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008, Lecture Notes in Computer Science 4963 [doi:10.1007/978-3-540-78800-3_1]

See also:

On hardware verification using proof assistants:

  • Mark Aagaard, Miriam Leeser, A methodology for efficient hardware verification, Formal Methods in System Design 5 (1994) 95-117 [doi:10.1007/BF01384235]

On hardware verification of quantum computing-systems:

Last revised on February 26, 2024 at 12:41:54. See the history of this page for a list of all contributions to it.