News for hackers. Stuff that matters.
Re:Total Functional Programming [pdf] by tome on Thursday October 06, 2016 @05:26PM (#12656250)
> it is a common error -- but an error nonetheless -- to believe that totality has a non-negligible effect on proving correctness of computations

Is it a common error? Who's commonly saying this? Can you link any examples? It seems a really strange claim to make.

Re:Total Functional Programming [pdf] by pron on Friday October 07, 2016 @01:36AM (#12658423)
> Can you link any examples

There are a couple in this very discussion:

https://news.ycombinator.com/item?id=12648261

https://news.ycombinator.com/item?id=12648932

A quick Google search I did just now came up with this one, by someone who knows better[1]: By writing programs in a total language like this, you can confidently answer questions that you can't with a Turing-complete language. You've overcome theoretical limitations by changing the problem parameters a little bit—a common approach in engineering.

The only question you can confidently answer is "does the program halt", to which the answer is always yes. You cannot confidently answer any other question any easier than in non-total languages.

You can find more examples in recent discussions about the Ethereum heist, with many suggestions to "just use a non-Turing complete language". Many seem to believe that there are languages that make verification easy, or that Turing completeness is the problem.

> It seems a really strange claim to make

I guess the reasoning goes like this: the impossibility of proving things in general about programs is a result of the halting theorem; we can get around the halting theorem by using languages that only admit programs that halt; assuming the language is still useful -- problem solved!

How many people know about bounded halting? I know I hadn't until rather recently, when I thought about it and somebody pointed out to me that it's at the very core of the time-hierarchy theorem. I think I actually thought about it because of total languages, when I realized that every program can be assumed to be total without loss of generality, and so totality cannot add actionable information.

[1]: https://www.quora.com/Can-we-solve-the-halting-problem-by-de...