4 ms·

Fun fact: even theorem provers have counterexamples - Breaking Badfny: https://www.reddit.com/r/Coq/comments/x4d31y/breaking_badfny/ https://www.reddit.com/r/C

Fun fact: even theorem provers have counterexamples - Breaking Badfny: https://www.reddit.com/r/Coq/comments/x4d31y/breaking_badfny/ https://www.reddit.com/r/Coq/comments/x4d31y/breaking_badfny... - Falso (Coq): https://github.com/clarus/falso https://github.com/clarus/falso - Coq critical bugs (some of these mention potential ways to prove false): https://github.com/coq/coq/blob/master/dev/doc/critical-bugs https://github.com/coq/coq/blob/master/dev/doc/critical-bugs (You can also get the theorem prover itself to hang or crash; if you work with theorem provers often, you'll even do this unintentionally, many times!)

gnulinux 3y ago
Not just simple counterexamples (i.e. programming "bugs"), some theorem provers have systematic bugs that were discovered later and required programming language change because people building it weren't sure how to fix it, mathematically speaking. For example, in Agda, there are two ways to create coinductive types. The most liberal and useful one uses a technique called "Sized Types". Sized Types are types where you annotate each type with a compile type upperbound "size" which allows compiler to prove a given coinductive computation on this object will terminate. You can image a conductive list "List T i" where "i" is a "Size Type". Ultimately, the compiler implements this using a mix of lazy evaluation and bookkeeping upperbounds using natural numbers. Originally, this was part of the "safe" subset of the language. Meaning, you can write Agda code using Sized Types, and Agda compiler claims the subset of the language you use is sound. This means you cannot prove inconsistencies. Here comes this "bug" which showed otherwise: https://github.com/agda/agda/issues/1201 https://github.com/agda/agda/issues/1201 Since 2015 Agda developers have been working on ways to mitigate this problem. Finding no such solution, they eventually decided in May 2021 to remove Sized Types from the "safe" subset of the language: https://github.com/agda/agda/pull/5354 https://github.com/agda/agda/pull/5354
- nerdponx 3y ago
  It's probably worth distinguishing between "compiler bugs" and "fundamental theoretical problems". From what I've seen of Idris 2 development, sometimes what looks like the former turns out to be the latter. But what I find really cool is that the theoretical problems are not necessarily unsolvable, and there seems to be a steady stream of new theoretical results that find their way into compilers. So even if we are a very long way off from these languages gaining wide adoption, it's exciting to see that progress is in fact being made, even if it's slow.
- Analemma_ 3y ago
  This is not my area of expertise, but I clicked around those Agda bugs with some interest, and it seems like all those problems are stemming from the fact that they defined inf < inf. A couple people mentioned addressing the issue by getting rid of that, and others objected that it would cause more problems than it solved. What are those problems? Why is inf < inf?
  - HappyPanacea 3y ago
    This is also not my area of expertise, but considering they are using sized types to prove termination through well-foundness so they are probably suppose to be ordinals where we can have ω < ω+1 but for some reasons they decide to forgo to distinguish between everything larger than ω and denote it as inf. Edit: I found an explanation https://ionathan.ch/2021/08/04/sized-types.html https://ionathan.ch/2021/08/04/sized-types.html
nickdrozd 3y ago
> You can also get the theorem prover itself to hang or crash; if you work with theorem provers often, you'll even do this unintentionally, many times! Proving something false is a grave sin for a prover. On the other hand, failing to prove something true is not only forgivable, but inevitable as per the incompleteness theorem. While ideally this failure would presented in terms of a nice error message, crashes are preferable to unsoundness. Crashes can even be deliberately induced as a defensive measure: https://hal.science/hal-04096390/document https://hal.science/hal-04096390/document
- CHY872 3y ago
  It really depends on how automated the prover is, this is kind of like reinforcement learning optimising something unintentionally. Theorem prover bugs are problematic if relied upon, but most of the bugs folks cite are only usable in very strange circumstances, and most practitioners will not see their results invalidated by such a bug. E.g. iirc falso required a type with more than 256 variants. If you don’t have one of those, it won’t affect you! Essentially, you fix the bug, re-run your hol or whatever, and hope your theorem is still true. Obviously this only applies to bugs in the implementation as opposed to an unsound logic.
- IIAOPSW 3y ago
  I feel like getting stuck in an infinite loop is a more appropriate encoding of "undecidable"
mananaysiempre 3y ago
The tongue-in-cheek MOTD of the Agda IRC channel outright says “We last proved false at ...”. Of course, Agda is somewhat unusual because they are kind of making up the (very strong) logical theory as they go along instead of having a fixed core logic they could dump proofs in for double-checking, like Coq. On the flip side, Agda actually makes for a halfway usable programming language—unlike Coq.

gnulinux 3y ago

Not just simple counterexamples (i.e. programming "bugs"), some theorem provers have systematic bugs that were discovered later and required programming language change because people building it weren't sure how to fix it, mathematically speaking. For example, in Agda, there are two ways to create coinductive types. The most liberal and useful one uses a technique called "Sized Types". Sized Types are types where you annotate each type with a compile type upperbound "size" which allows compiler to prove a given coinductive computation on this object will terminate. You can image a conductive list "List T i" where "i" is a "Size Type". Ultimately, the compiler implements this using a mix of lazy evaluation and bookkeeping upperbounds using natural numbers. Originally, this was part of the "safe" subset of the language. Meaning, you can write Agda code using Sized Types, and Agda compiler claims the subset of the language you use is sound. This means you cannot prove inconsistencies. Here comes this "bug" which showed otherwise: https://github.com/agda/agda/issues/1201 https://github.com/agda/agda/issues/1201 Since 2015 Agda developers have been working on ways to mitigate this problem. Finding no such solution, they eventually decided in May 2021 to remove Sized Types from the "safe" subset of the language: https://github.com/agda/agda/pull/5354 https://github.com/agda/agda/pull/5354

nerdponx 3y ago
It's probably worth distinguishing between "compiler bugs" and "fundamental theoretical problems". From what I've seen of Idris 2 development, sometimes what looks like the former turns out to be the latter. But what I find really cool is that the theoretical problems are not necessarily unsolvable, and there seems to be a steady stream of new theoretical results that find their way into compilers. So even if we are a very long way off from these languages gaining wide adoption, it's exciting to see that progress is in fact being made, even if it's slow.
Analemma_ 3y ago
This is not my area of expertise, but I clicked around those Agda bugs with some interest, and it seems like all those problems are stemming from the fact that they defined inf < inf. A couple people mentioned addressing the issue by getting rid of that, and others objected that it would cause more problems than it solved. What are those problems? Why is inf < inf?
- HappyPanacea 3y ago
  This is also not my area of expertise, but considering they are using sized types to prove termination through well-foundness so they are probably suppose to be ordinals where we can have ω < ω+1 but for some reasons they decide to forgo to distinguish between everything larger than ω and denote it as inf. Edit: I found an explanation https://ionathan.ch/2021/08/04/sized-types.html https://ionathan.ch/2021/08/04/sized-types.html

nickdrozd 3y ago

> You can also get the theorem prover itself to hang or crash; if you work with theorem provers often, you'll even do this unintentionally, many times! Proving something false is a grave sin for a prover. On the other hand, failing to prove something true is not only forgivable, but inevitable as per the incompleteness theorem. While ideally this failure would presented in terms of a nice error message, crashes are preferable to unsoundness. Crashes can even be deliberately induced as a defensive measure: https://hal.science/hal-04096390/document https://hal.science/hal-04096390/document

CHY872 3y ago
It really depends on how automated the prover is, this is kind of like reinforcement learning optimising something unintentionally. Theorem prover bugs are problematic if relied upon, but most of the bugs folks cite are only usable in very strange circumstances, and most practitioners will not see their results invalidated by such a bug. E.g. iirc falso required a type with more than 256 variants. If you don’t have one of those, it won’t affect you! Essentially, you fix the bug, re-run your hol or whatever, and hope your theorem is still true. Obviously this only applies to bugs in the implementation as opposed to an unsound logic.
IIAOPSW 3y ago
I feel like getting stuck in an infinite loop is a more appropriate encoding of "undecidable"

mananaysiempre 3y ago

The tongue-in-cheek MOTD of the Agda IRC channel outright says “We last proved false at ...”. Of course, Agda is somewhat unusual because they are kind of making up the (very strong) logical theory as they go along instead of having a fixed core logic they could dump proofs in for double-checking, like Coq. On the flip side, Agda actually makes for a halfway usable programming language—unlike Coq.