4 ms·

There exist research programming languages that support 'total functions', that can be proven to always halt. Usually you divide the world into functions and co

There exist research programming languages that support 'total functions', that can be proven to always halt. Usually you divide the world into functions and cofunctions, and data and codata, the latter of which may be infinite (such as I/O). I wish this were a more popular thing. When I write a function, I can probably enumerate in my head all the things I want it to do, and not halting usually isn't one of those things. But the instinctive reaction is to worry about Turing-completeness, which is puzzling. When's the last time you wanted a program with fundementally unprovable behavior?

Ezku 13y ago
Programming with such functions is called total functional programming. Here's a nice little introduction to the subject[1], and if you're a fan of code and math you should probably check out the other blog entries as well. [1]: http://blog.sigfpe.com/2007/07/data-and-codata.html http://blog.sigfpe.com/2007/07/data-and-codata.html
btilly 13y ago
When's the last time you wanted a program with fundementally unprovable behavior? I'm working on one today. I'm analyzing a data set for tens of millions of possible statistical anomalies, and I'm putting my "investigate further" threshold to statistically one in billions. Each thing added increases the size of the search space. Knowing that it is extremely unlikely to run forever really is good enough. Proving that it won't is a non-issue for me. (Right now it takes several hours to run.)
Alphasite_ 13y ago
AI?
dragonwriter 13y ago
> When I write a function, I can probably enumerate in my head all the things I want it to do, and not halting usually isn't one of those things. But the instinctive reaction is to worry about Turing-completeness, which is puzzling. When's the last time you wanted a program with fundementally unprovable behavior? You don't usually want fundamentally unprovable behavior. However, you also don't want to sacrifice the ability to compute anything that is computable. And you can't throw out the bathwater of the halting problem without throwing out the baby of computing everything computable. So, in practice, you want to use provably-halting-on-all-valid-inputs algorithms for the problems where you have available (either known, or that you can find with reasonable effort) such an algorithm, but retain the option of using other techniques for other problems.

Ezku 13y ago

Programming with such functions is called total functional programming. Here's a nice little introduction to the subject[1], and if you're a fan of code and math you should probably check out the other blog entries as well. [1]: http://blog.sigfpe.com/2007/07/data-and-codata.html http://blog.sigfpe.com/2007/07/data-and-codata.html

btilly 13y ago

When's the last time you wanted a program with fundementally unprovable behavior? I'm working on one today. I'm analyzing a data set for tens of millions of possible statistical anomalies, and I'm putting my "investigate further" threshold to statistically one in billions. Each thing added increases the size of the search space. Knowing that it is extremely unlikely to run forever really is good enough. Proving that it won't is a non-issue for me. (Right now it takes several hours to run.)

Alphasite_ 13y ago

AI?

dragonwriter 13y ago

> When I write a function, I can probably enumerate in my head all the things I want it to do, and not halting usually isn't one of those things. But the instinctive reaction is to worry about Turing-completeness, which is puzzling. When's the last time you wanted a program with fundementally unprovable behavior? You don't usually want fundamentally unprovable behavior. However, you also don't want to sacrifice the ability to compute anything that is computable. And you can't throw out the bathwater of the halting problem without throwing out the baby of computing everything computable. So, in practice, you want to use provably-halting-on-all-valid-inputs algorithms for the problems where you have available (either known, or that you can find with reasonable effort) such an algorithm, but retain the option of using other techniques for other problems.