3 ms·

I'm with you almost everywhere, but it's worth pondering this: > If a program is accepted by the proof checker, then by construction it must be a valid mathema

I'm with you almost everywhere, but it's worth pondering this: > If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof. I'd phrase it as "If a program is accepted by a _correct_ proof checker, then ...". That makes it clear that we can't escape having to consider how and why the proof checker is considered correct. Edit: this is not entirely academic. from what I understand, the unsoundness of Hindley-Milner in the presence of polymorphic references was not immediately known (https://en.wikipedia.org/wiki/Value_restriction#A_Counter_Example_to_Type_Safety https://en.wikipedia.org/wiki/Value_restriction#A_Counter_Ex...).

markisus 3y ago
This is a great point. In a computer proof system, you produce judgements like "the term x has type is T", where the type "T" encodes the statement of a theorem and "x" is the proof. We must be certain that whenever the type checker verifies that "x has type T", it means that the theorem "T" is actually true. Such a meta-proof must be done on pen and paper, before any code is written at all. Any bug in this meta-proof would destroy our ability to rely on the computer proof system.
- cscheid 3y ago
  > Such a meta-proof must be done on pen and paper, before any code is written at all. Not so fast; it could be done on a _different automated system_ (say, a smaller one) than the one you're building, in which case you're now relying on that system's correctness. Or it could even not be proven at all. This is not too different from what mathematicians do when they (often) say "assuming P != NP", or "assuming GRH", or "assuming FLT", etc etc. It's simply that it's worth being careful and precise.
wk_end 3y ago
To be ruthlessly, uselessly pedantic - after all, we're mathematicians - there's reasonable definitions of "academic" where logical unsoundness is still academic if it never interfered with the reasoning behind any proofs of interest ;) But: so long as we're accepting that unsoundness in your checker or its underlying theory are intrinsically deal breakers, there's definitely a long history of this, perhaps somewhat more relevant than the HM example, since no proof checkers of note, AFAIK, have incorporated mutation into their type theory. For one thing, the implementation can very easily have bugs. Coq itself certainly has had soundness bugs occasionally [0]. I'm sure Agda, Lean, Idris, etc. have too, but I've followed them less closely. But even the underlying mathematics have been tricky. Girard's Paradox broke Martin-Löf's type theory, which is why in these dependently typed proof assistants you have to deal with the bizarre "Tower of Universes"; and Girard's Paradox is an analogue of Russell's Paradox which broke more naive set theories. And then Russell himself and his system of universal mathematics was very famously struck down by Gödel. But we've definitely gotten it right this time... [0] https://github.com/coq/coq/issues/4294 https://github.com/coq/coq/issues/4294
- tshaddox 3y ago
  > there's reasonable definitions of "academic" where logical unsoundness is still academic if it never interfered with the reasoning behind any proofs of interest ;) I wouldn't really so. If you were relying on the type system to tell you about any errors you made in your program, the revelation that your type system was unsound is not "only academic" simply because your program coincidentally didn't have errors. Just like it wouldn't be "only academic" if you discovered that your car's airbags weren't functional for the last 10 years even though you never had any accidents.
  - llm_thr 3y ago
    [dead]
hnfong 3y ago
I'd also note that the correctness of the proof checker not only lies in the high level software code, but also the full stack of hardware down to the nanoscale. Eg. - Are you sure the compiler is correct? - Are you sure the OS is behaving correctly? - Are you sure the CPU isn't randomly glitching out? There's a difference between believing that these things are correct 99.999% of the time, and claiming that it's mathematically proven to behaving correctly. Mathematical proof isn't statistics, so either you're willing to claim and defend the claim that the whole stack of the proof checker is correct, or you don't have a proof at all. How one would prove that a physical modern CPU conforms to a formal spec I have no idea TBH. I presume the QA of chip manufacturers uses statistical methods.
- galaxyLogic 3y ago
  > Are you sure the compiler is correct? Use multiple different compilers and compare results > Are you sure the OS is behaving correctly? Use multiple different OSes and OS-versions > Are you sure the CPU isn't randomly glitching out? Use multiple different CPU types.

markisus 3y ago

This is a great point. In a computer proof system, you produce judgements like "the term x has type is T", where the type "T" encodes the statement of a theorem and "x" is the proof. We must be certain that whenever the type checker verifies that "x has type T", it means that the theorem "T" is actually true. Such a meta-proof must be done on pen and paper, before any code is written at all. Any bug in this meta-proof would destroy our ability to rely on the computer proof system.

cscheid 3y ago
> Such a meta-proof must be done on pen and paper, before any code is written at all. Not so fast; it could be done on a _different automated system_ (say, a smaller one) than the one you're building, in which case you're now relying on that system's correctness. Or it could even not be proven at all. This is not too different from what mathematicians do when they (often) say "assuming P != NP", or "assuming GRH", or "assuming FLT", etc etc. It's simply that it's worth being careful and precise.

wk_end 3y ago

To be ruthlessly, uselessly pedantic - after all, we're mathematicians - there's reasonable definitions of "academic" where logical unsoundness is still academic if it never interfered with the reasoning behind any proofs of interest ;) But: so long as we're accepting that unsoundness in your checker or its underlying theory are intrinsically deal breakers, there's definitely a long history of this, perhaps somewhat more relevant than the HM example, since no proof checkers of note, AFAIK, have incorporated mutation into their type theory. For one thing, the implementation can very easily have bugs. Coq itself certainly has had soundness bugs occasionally [0]. I'm sure Agda, Lean, Idris, etc. have too, but I've followed them less closely. But even the underlying mathematics have been tricky. Girard's Paradox broke Martin-Löf's type theory, which is why in these dependently typed proof assistants you have to deal with the bizarre "Tower of Universes"; and Girard's Paradox is an analogue of Russell's Paradox which broke more naive set theories. And then Russell himself and his system of universal mathematics was very famously struck down by Gödel. But we've definitely gotten it right this time... [0] https://github.com/coq/coq/issues/4294 https://github.com/coq/coq/issues/4294

tshaddox 3y ago
> there's reasonable definitions of "academic" where logical unsoundness is still academic if it never interfered with the reasoning behind any proofs of interest ;) I wouldn't really so. If you were relying on the type system to tell you about any errors you made in your program, the revelation that your type system was unsound is not "only academic" simply because your program coincidentally didn't have errors. Just like it wouldn't be "only academic" if you discovered that your car's airbags weren't functional for the last 10 years even though you never had any accidents.
- llm_thr 3y ago
  [dead]

hnfong 3y ago

I'd also note that the correctness of the proof checker not only lies in the high level software code, but also the full stack of hardware down to the nanoscale. Eg. - Are you sure the compiler is correct? - Are you sure the OS is behaving correctly? - Are you sure the CPU isn't randomly glitching out? There's a difference between believing that these things are correct 99.999% of the time, and claiming that it's mathematically proven to behaving correctly. Mathematical proof isn't statistics, so either you're willing to claim and defend the claim that the whole stack of the proof checker is correct, or you don't have a proof at all. How one would prove that a physical modern CPU conforms to a formal spec I have no idea TBH. I presume the QA of chip manufacturers uses statistical methods.

galaxyLogic 3y ago
> Are you sure the compiler is correct? Use multiple different compilers and compare results > Are you sure the OS is behaving correctly? Use multiple different OSes and OS-versions > Are you sure the CPU isn't randomly glitching out? Use multiple different CPU types.