Lawrence C. Paulson

Great article, two minor nitpicks:

> To avoid Russell's Paradox, there isn't a type of all types. Instead, we have universes.

This is an oversimplification, and Lean-specific (to be fair, the author claims to explore these concept in Lean). Girard's paradox comes from unrestricted impredicativity. To maintain consistency one needs to control impredicativity, type universes are a possible, very straightforward choice, but it is not the only choice.

Some theorem provers, such as Cedille, do not use type universes, and even have `Type : Type` while still being consistent. See Stump, Aaron: “The Calculus of Dependent Lambda Eliminations.” Journal of Functional Programming 27 (2017): e14. DOI:10.1017/S0956796817000053[0]

Additionally:

> The famous Curry-Howard correspondence states [...] Propositions are types in Prop [...]

Curry-Howard doesn't say anything about Prop, Prop vs. Type is just a distinction done in some particular type theories for pragmatic reasons, or because it simplifies classical (as opposed to intuitionistic) reasoning. In fact the reason why Prop vs. Type is a distinction done by many theorem provers leads Lawrence Paulson[1] to claim that modern theorem provers don't really use Curry-Howard[2], at least as Curry-Howard was originally defined. I disagree, because elements of Prop are still types, but please understand that this is a departure from original Curry-Howard.

Moreover:

> The famous Curry-Howard correspondence states [...] True propositions…

Well, at some point you have to define what you mean by "proof by contradiction". I was responding to your statement, "prove something by showing that the alternative is unsound". You can prove that something is false that way without needing classical logic.

Mathlib defines `by_contradiction` as a theorem proving `(¬p → False) → p` for any proposition p. ( https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Basic.html#by_contradiction ) This does require classical logic.

For what's happening with `¬p -> F`, recall that this is by definition the statement `¬¬p`; classical logic will let you conclude `p` from `¬¬p`, or it will let you apply the law of the excluded middle to conclude that either `p` or `¬p` must be the case, and then show that since it isn't `¬p`, it must be `p`. (Again, not really different approaches, but perhaps different in someone's mental model.)

On the other hand, if you have `p -> F`, that is by definition the statement `¬p`, and if you've established `¬p`, you've already finished proving that p is false.

Something that I find particularly absurd about the hypothetical distinction between intuitionistic and classical logic is that intuitionistic logic is sufficient to prove `¬p` from `¬¬¬p`. (This is quite similar to how 'proof by contradiction' is constructive if you're proving a negative but not if you're proving a positive; it might be the same result.) So for any proposition that can be restated in a "negative" way, the law of…

> Formally proving with a system based on probabilities (temperature, etc.) is for me an oxymoron. But I am not a mathematician.

In the context of automated theorem proving, proof search and proof checking could not be more different.

Proof search is undecidable for most logics. For that reason, heuristics are commonly used to guide proof search. This has always been the case; heuristic proof search predates the use of LLMs for theorem proving by decades.

Proof checking, on the other hand, is not just decidable but usually quite tractable and cheap. Therefore, proof checkers are typically deterministic and fast. Ideally the checker is also implemented in small amount of relatively simple and heavily audited code.

For a high-level description of how provers are typically architected, see https://www.pls-lab.org/en/de_Bruijn_criterion (or https://lawrencecpaulson.github.io/2022/01/05/LCF.html which is linked to at the bottom of the above page and goes into a bit more historical detail and nuance).

> I am not sure if this is better than generating cooking recipes with a LLM and asking a cook if they make sense or not.

Conceptually it's not at all similar to asking a cook if a recipe is "correct". For lean proofs, "correct" has an entirely precise meaning. The "cook" (i.e., proof checker) is basically free (much less than $0.01/hr). The cook (proof checker) takes at most a few seconds to read and respond to any particular recipe. And the cook (i.e., checker) never makes…

You have conveniently skipped the "Philosophical Objections" section in Wikipedia which i had pointed out and which would have given you some hints as to what i am saying.

> A proof of a program's correctness is mathematical in nature, it doesn't stand apart in some distinct non-mathematical realm ... I think this is really a disagreement on phraseology though, nothing deeper.

It is mathematical in nature but if the objects it deals with do not obey the axioms and/or the axioms are inconsistent the whole edifice falls. You can provide a perfectly "valid" proof but starting with wrong/inconsistent axioms. In computing since everything is a series of calculations it becomes quite important to make sure that you can carry-over the axioms in an algebra "as is" from pure mathematics to programming. In the example that i gave, the C language gives you multiple sets (aka types) of integers (i.e. cartesian product of {signed, unsigned} X {8, 16, 32, 64}) which are all subsets of the mathematical structure Z. You can distribute these types across the variables a/b/c in the expression in many different orders each of which have to be proven separately for the axiom of associativity to hold generally.

> Programming languages can be modelled mathematically. Programs can be modelled mathematically. That's much of the point of formal methods. Real computers are finite state machines. So what?

Mathematics is static/declarative while Computing has both static/structural and…

Another aspect of this is the readability of the resulting text. The role of a proof in mathematics is not only to certify that an assertion is true, but also to communicate to mathematicians why it is true. Lean and Coq verification scripts are not readable in this sense. They do certify that assertions of theorems are true and (at the current state of technology) that the author of the script most likely knows why they are true, but it is close to impossible for a reader to see what is going on in the proof without running the script step by step in software. The Mizar proof language and Isabelle/Isar were designed to communicate as well and proofs written in those languages can be read and understood directly by humans. For a comparison how the same proof of a simple theorem looks like in Lean, Isabelle/HOL, Isabelle/ZF and Mizar see [1], [2] and [3].

[1] https://lawrencecpaulson.github.io/2024/02/28/Gowers_bijection_example.html

[2] https://isarmathlib.org/func1.html#a_bij_def_alt

[3] https://mizar.uwb.edu.pl/forum/archive/2403/msg00001.html

(Original title shortened because it's too long.)

Why higher-order logic is a good formalisation for specifying and verifying hardware

Mike Gordon

September 1985, 28 pages

DOI https://doi.org/10.48456/tr-77

Abstract

Higher order logic was originally developed as a foundation for mathematics. In this paper we show how it can be used as: 1. a hardware description language, and 2. a formalism for proving that designs meet their specifications.

Examples are given which illustrate various specification and verification techniques. These include a CMOS inverter, a CMOS full adder, an n-bit ripple-carry adder, a sequential multiplier and an edge-triggered D-type register.

See also https://lawrencecpaulson.github.io/2023/01/04/Hardware_Verification.html and "Interactive Formal Verification, Lecture 11: Hardware Verification" by Lawrence Paulson https://www.youtube.com/watch?v=KVdgoEpo4uI&list=PLVdBoNna-44AN-hq4e3SZP-cbzFNtuV8g&index=13