3 ms·
> Almost any unproven mathematical conjecture, e.g. a program that searches for counterexamples to the Riemann hypothesis. This is a very good example. We don'
by schoen 2y ago
> Almost any unproven mathematical conjecture, e.g. a program that searches for counterexamples to the Riemann hypothesis.
This is a very good example. We don't know whether such programs will ever stop, and knowing is exactly equivalent to resolving the conjectures.
> More practically, a lot of problems reduce to SAT, so these days quite a lot of systems work by just running a SAT solver on the problem (e.g. dependency resolution in some build systems), and it's fast most of the time but you can never be sure it's not going to get stuck.
This is a less good example because SAT solvers can always run in finite time and can be proven to halt. Even if they do "get stuck", they will take exponential time rather than infinite time.
There are probably some problems that arise practically that are undecidable in general (e.g. type checking for sufficiently expressive type systems), but problems that "reduce to SAT" are never examples of such undecidable problems because SAT is decidable.
- musicale 2y agoI was going to say the same thing about SAT, or any NP-hard problem. The first example doesn't seem to be good either however. I don't think that proving a mathematical conjecture which has resisted proof for decades (or longer) is something that we would typically expect a computer program to be able to do. Whenever this happens, it is hailed as a major breakthrough.
- anyfoo 2y agoIs there some circular logic in your reasoning? What is the difference between the computer program solving the conjecture, and “us” doing it?
- lmm 2y agoThe point is that it can complicate analysis of a program, at least if you take the fundamentalist view that all program behaviour should be provably correct. Like if you need the collantz sequence of a number or something in your program, you would just calculate it and use it, but it's surprisingly hard to prove that it always exists. Which isn't so much a problem in itself as it complicates trying to prove anything else about your program's behaviour.