Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMay 10th 2012
    • (edited May 10th 2012)

    I created a stub certified programming.

    That’s motivated from me having expanded the Idea-section at type theory. I enjoyed writing the words “is used in industry”. There are not many nnLab pages where I can write these words.

    I am saying this only half-jokingly. Somehow there is something deep going on.

    Anyway, in (the maybe unlikely) case that somebody reading this here has lots of information about the use and relevance of certified programming in industry, I’d enjoy seeing more information added to that entry.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeMay 10th 2012

    One shouldn’t get too excited, though; certified programming as done in Coq and Agda hasn’t made many inroads in actual industry. The automation is just not there yet for it to be worth the time and effort.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 10th 2012

    A social historian, Donald MacKenzie wrote on the attempt to certify that a chip met a specification in his 2001 Mechanizing proof: computing risk, and trust Cambridge, MA:MIT Press. Apparently the case nearly came to court over whether this had been proved, but unfortunately the company went bust. Otherwise we would have heard lawyers thrashing out the nature of proof. See also MacKenzie D 1991 The fangs of the VIPER Nature 352 467–468.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJul 22nd 2015
    • (edited Jul 22nd 2015)

    I have added to the Idea-section at certified programming the following text, which appears as the description of the UK research grant titled Homotopy Type Theory: Programming and Verification:

    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 medallist 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.

    • CommentRowNumber5.
    • CommentAuthorTim_Porter
    • CommentTimeJul 22nd 2015
    • (edited Jul 22nd 2015)

    As I remember it when the idea of ’proof’ of software was being debated in a law court, the software engineers used ’prove’ in the engineering sense, i.e. ’test’ as in ’proved steel’. Unfortunately some people had understood ’prove’ in the mathematical sense. The lawyers for the engineers won that battle! (I am not sure when this happened and it may be misremembered, but there are two uses of ’prove’.)

    • CommentRowNumber6.
    • CommentAuthorzskoda
    • CommentTimeJul 22nd 2015
    • (edited Jul 22nd 2015)

    But every mathematical proof of a real life matter depends on the validity of overall assumptions and model which itself may be fundamentally flawed or missing essential influencing real-life parameters.

    • CommentRowNumber7.
    • CommentAuthorspitters
    • CommentTimeJul 23rd 2015
    • (edited Jul 23rd 2015)

    Tim, It would be nice to know a bit more about what you have in mind. Statistical proof is allowed in court (and there have been some horrible accidents ). Most cryptographic proofs are statistical in nature.

    • CommentRowNumber8.
    • CommentAuthorTim_Porter
    • CommentTimeJul 23rd 2015
    • (edited Jul 23rd 2015)

    I cannot remember the details. Statistically based testing had been used and won the day in court, because the company who produced the chip could claim that they had ’proved’ that the chip was fault free. They also claimed that their advertising for the product in using ’proved’ had been misunderstood by the person who was claiming damages and that with common (engineering) usage their advertising was correct, and there had been no intent to deceive. (It may have been a chip for a pocket calculator that was in question. I do not recall, as I said.)

    I have a very vague thought that the detected fault was in something that was a simple calculation, something like a ‘tan’ and because of the type of sample calculations that had been used in the testing, it had not been detected.

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 1st 2015

    The old sense of “prove” mentioned in #5, meaning “to test”, is in such sayings as “the exception proves the rule” and “the proof is in the pudding”, and obviously in phrases such as “proving grounds”. I would have thought the distinction in meaning is very familiar in legal circles (although obviously IANAL).

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeOct 15th 2019

    The entry still quotes this remarkable claim, from the EPSRC research grant Homotopy Type Theory: Programming and Verification, which says (in drastically shortened quote):

    The cost of software failure is truly staggering. [][\cdots] a fundamental and difficult problem which has remained unresolved for over 40 years. But now it looks like we might have a solution! [][\cdots] namely homotopy theory, leading to Homotopy Type Theory (HoTT).

    I see that this grant has run out just last month. Can one say anything in update of these claims?

    diff, v7, current

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeFeb 17th 2021

    fixed the link for

    (now via WaybackMachine)

    and added a reference on verification of quantum programming languages such as Quipper:

    • 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, vol 9720. Springer, Cham (doi:10.1007/978-3-319-40578-0_16)

    diff, v9, current

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    added pointer to:

    diff, v10, current

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    added this pointer:

    • Aleksandar Nanevski, Anindya Banerjee, Deepak Garg, Dependent Type Theory for Verification of Information Flow and Access Control Policies, ACM Transactions on Programming Languages and Systems July 2013 Article No.: 6 (arXiv:10.1145/2491522.2491523)

    diff, v10, current

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    added this pointer:

    also subdivided the list of references into subsections

    diff, v10, current

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    also this one:

    diff, v10, current

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    added this pointer:

    • Adam Petcher, Greg Morrisett, The Foundational Cryptography Framework, In: R. Focardi, A. Myers (eds.) Principles of Security and Trust POST 2015. Lecture Notes in Computer Science, vol 9036. Springer, Berlin, Heidelberg (doi:10.1007/978-3-662-46666-7_4)

    diff, v10, current

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    and this one:

    diff, v10, current

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    and this one:

    diff, v10, current

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    and this:

    • 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)

    diff, v10, current

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    and this one:

    • 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)

    diff, v10, current

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    and this one:

    • Mihhail Aizatulin, Verifying Cryptographic Security Implementations in C Using Automated Model Extraction (arXiv:2001.00806)

    diff, v10, current

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    also this:

    • Andrew W. Appel, Verification of a Cryptographic Primitive: SHA-256, ACM Transactions on Programming Languages and SystemsApril 2015 Article No.: 7 (doi:10.1145/2701415, pdf)

    diff, v10, current

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    added this one:

    • 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, Volume 25: Logics and Languages for Reliability and Security (doi:10.3233/978-1-60750-100-8-1)

    diff, v10, current

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2021

    added this pointer:

    diff, v12, current

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    added pointer to:

    diff, v15, current

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeJun 17th 2022

    added (here) more references on verification of quantum programs/circuits

    diff, v17, current

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeNov 7th 2022

    added pointer to:

    and

    diff, v18, current

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2022

    added pointer to:

    diff, v19, current

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeJan 17th 2023

    added pointer to:

    diff, v26, current

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeJan 18th 2023

    added (here) pointer to:

    diff, v27, current

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeFeb 19th 2023

    added pointer to:

    diff, v29, current

    • CommentRowNumber32.
    • CommentAuthorUrs
    • CommentTimeFeb 24th 2023

    Added a couple of references on hardware verfication (here)

    diff, v31, current

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeFeb 24th 2023

    added pointer to:

    diff, v31, current

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeFeb 24th 2023

    added pointer to:

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

    diff, v31, current

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeMar 3rd 2023

    added pointer to

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

    and this quote from its abstract (which however seems to only appear on the webpage behind the DOI, but not in the actual book):

    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.

    diff, v32, current

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeMar 3rd 2023
    • (edited Mar 3rd 2023)

    added pointer to:

    • 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]

    with this quote (reiterating a point which may have been first voiced by Rand (2018)):

    “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.”

    diff, v32, current

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeMar 3rd 2023

    added pointer to:

    • 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]

    with this quote:

    “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.”

    diff, v32, current

    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeMar 3rd 2023

    added pointer to:

    with this quote:

    “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.”

    diff, v32, current

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeMar 3rd 2023

    added pointer to:

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

    diff, v32, current

    • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTimeMar 3rd 2023

    added pointer to:

    diff, v32, current

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeMar 6th 2023
    • CommentRowNumber42.
    • CommentAuthorUrs
    • CommentTimeMar 6th 2023

    added pointer to:

    diff, v34, current

    • CommentRowNumber43.
    • CommentAuthorUrs
    • CommentTimeJul 13th 2023
    • (edited Jul 13th 2023)

    more references:

    diff, v35, current

    • CommentRowNumber44.
    • CommentAuthorUrs
    • CommentTimeAug 16th 2023
    • (edited Aug 16th 2023)

    added pointer to

    with this quote:

    [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.”

    (Previously I used to think that Rand 2018 was the first to make this point so explicitly.)

    diff, v37, current

    • CommentRowNumber45.
    • CommentAuthorUrs
    • CommentTimeFeb 26th 2024

    added pointer to:

    diff, v40, current