3 ms·

Not just simple counterexamples (i.e. programming "bugs"), some theorem provers have systematic bugs that were discovered later and required programming languag

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

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