Yes and no, but more yes than no. My counterexample is that we had a big glut of NoSQL databases for a few years there in which everyone seemed to be providing constructive proofs of their ideas about distributed data storage, except that it took Aphyr’s tests to prove that many of those ideas didn’t really work, they only sort of appeared to work because they were never really tested under the conditions they claimed to support.

This is one of the reasons I like math though. There are things you could never prove by constructing software, which you can nevertheless prove with math—the CAP theorem comes to mind. But a constructive proof in math is not exactly the same thing as a practical program you can run. (In theory, they might be.)

I have mixed feelings about this. On the one hand, such a tool would be useful and cool, and would certainly make it easier to stomp on some crank’s program. On the other hand, I feel like we’re sort of losing sight of what proof is, and replacing it with a kind of faith in a certain program.

First idea that popped into my head is that this is only applicable if the thing in question is constructible. Non-existence is not constructible by its nature: I can prove to you that no decision procedure for the halting problem exists, but I cannot show this constructively.

Huh, TIL. Indeed, it seems that there exist proofs of the undecidability of the halting problem that are constructive.

¬ (A ∧ ¬ A) is apparently provable in intuitionistic logic, which suffices for diagonalization arguments:

lemma "¬ (A ∧ ¬ A)"
proof (rule notI)
assume 1: "A ∧ ¬ A"
from 1 have "A" by (rule conjE)
from 1 have "¬ A" by (rule conjE)
from `¬ A` `A` show False by (rule notE)
qed

The general point still stands though, as there are other examples, such as non-constructive existence proofs.

In general Coq proofs are not necessarily constructive, since one can define the law of the excluded middle as an axiom in Coq (and this is done in e.g. Coq.Classical). I can’t say anything about the proofs you linked though, as my Coq-foo is very limited.

I think, the way the definitions expand in that repo, that undecidable (HaltTM 1) is decidable (HaltTM 1) -> decidable (HaltTM 1), which is trivially true. That is, it’s taken as an axiom that Turing machines are undecidable. (I think? I might be misreading)

while Coq proofs are constructive, proving “~ exists t, t determines halting” does not construct any Turing machines, what it constructs is something that takes a hypothetical existence proof and builds a proof of false from it.

i.e. in construct math, ~ P is a function P -> False. this function can never be invoked as you can never build a P object.

As this post was tagged practices (not math) and the article addresses the difficulty of convincing people, I suspect you’ve misunderstood the author’s use of the phrase “constructive proof.”

Just for future reference, “constructive proof” is a term from math and I meant my usage of the term to be an analogy to math. Math also involves convincing people. But maybe I should have tagged it computer science or math, sorry.

Yes and no, but more yes than no. My counterexample is that we had a big glut of NoSQL databases for a few years there in which everyone seemed to be providing constructive proofs of their ideas about distributed data storage, except that it took Aphyr’s tests to prove that many of those ideas didn’t really work, they only sort of

appearedto work because they were never really tested under the conditions they claimed to support.This is one of the reasons I like math though. There are things you could never prove by constructing software, which you can nevertheless prove with math—the CAP theorem comes to mind. But a constructive proof in math is not exactly the same thing as a practical program you can run. (In theory, they might be.)

Perhaps you could constructively prove the CAP theorem with a testing tool that can break any database.

I have mixed feelings about this. On the one hand, such a tool would be useful and cool, and would certainly make it easier to stomp on some crank’s program. On the other hand, I feel like we’re sort of losing sight of what proof is, and replacing it with a kind of faith in a certain program.

First idea that popped into my head is that this is only applicable if the thing in question is constructible. Non-existence is not constructible by its nature: I can prove to you that no decision procedure for the halting problem exists, but I cannot show this constructively.

I would really like to learn more about this, aren’t coq proofs constructive by nature?

Here is a proof that the halting problem for turing machines is undecidable: https://github.com/uds-psl/coq-library-undecidability/blob/30d773c57f79e1c5868fd369cd87c9e194902dee/theories/TM/TM_undec.v#L8-L12

There are other proofs in that repo that show other problems as being undecidable.

Huh, TIL. Indeed, it seems that there exist proofs of the undecidability of the halting problem that are constructive.

`¬ (A ∧ ¬ A)`

is apparently provable in intuitionistic logic, which suffices for diagonalization arguments:The general point still stands though, as there are other examples, such as non-constructive existence proofs.

In general Coq proofs are not necessarily constructive, since one can define the law of the excluded middle as an axiom in Coq (and this is done in e.g. Coq.Classical). I can’t say anything about the proofs you linked though, as my Coq-foo is very limited.

I think, the way the definitions expand in that repo, that

`undecidable (HaltTM 1)`

is`decidable (HaltTM 1) -> decidable (HaltTM 1)`

, which is trivially true. That is, it’s taken as an axiom that Turing machines are undecidable. (I think? I might be misreading)while Coq proofs are constructive, proving “~ exists t, t determines halting” does not construct any Turing machines, what it constructs is something that takes a hypothetical existence proof and builds a proof of false from it.

i.e. in construct math, ~ P is a function P -> False. this function can never be invoked as you can never build a P object.

As this post was tagged practices (not math) and the article addresses the difficulty of

convincingpeople, I suspect you’ve misunderstood the author’s use of the phrase “constructive proof.”Mathematical (constructive proof) vs rhetorical (constructive criticism).

I don’t feel like the author talks about constructive criticism at all, how did you come to that conclusion?

☝🏾

Just for future reference, “constructive proof” is a term from math and I meant my usage of the term to be an analogy to math. Math also involves convincing people. But maybe I should have tagged it computer science or math, sorry.