As far as I've heard, Haskell's type system doesn't normally prove functions to be total; they can diverge. This fine, though, because for ordinary programming, a proof of totality isn't a useful guarantee. You care how long programs actually take to run, not whether they would theoretically finish eventually.
It's only when proving theorems that a mathematical proof of totality matters, and there are specialized languages for that.
For most people, we test in order to make a scientific claim, that we tried running it, and it worked for the inputs we tried, and completed in a reasonable amount of time.
This is true of property testing and even model-checking; in simple cases, sometimes an exhaustive test can be done, but they don't actually prove statements outside the bounds used when testing.
It's perfectly feasible to have proofs about programs together with a guaranteed upper bound on (something like) the "number of processor instructions it will take" (given known finite bounds for all inputs).
Of course, just like any other system that allows correctness proofs, it wouldn't be nearly useful enough to justify the effort for all but a negligible number of applications. That's at least until the levels of effort required are significantly reduced.
Yes, a theoretical calculation like that would be useful as an estimate. But theoretical performance on ideal machines is only loosely related to performance on real machines under real conditions. That's true of testing, too. Benchmark performance varies even between runs.
So there's still going to be a theoretical math versus science and engineering divide.
Another perspective is that we have a useful division of concerns. Static checking is useful to find some kinds of errors. API's help to ensure that certain things don't change in a new version, so that performance improvements are less likely to break callers.
Depending on the domain, leaving some things like performance and size limits deliberately unspecified in API's seems like more of a feature than a bug? Stricter interfaces aren't always an improvement.
> leaving some things like performance and size limits deliberately unspecified in API's seems like more of a feature than a bug
In rare cases there might be exceptions. Hard real time applications and constant time cryptography come to mind.
Regardless, I didn't mean for such proofs to be part of an API or any kind of interface. It's just a guarantee you would get about your program. E.g., "it never times out", or "the worst case data throughout is X" (in whatever hardware model the proof assumes, which in theory could be made very close to the actual hardware).
> As far as I've heard, Haskell's type system doesn't normally prove functions to be total; they can diverge.
This is true. You can write a function which is the natural numbers, and I wouldn't want the type system to preclude it.
nats :: [Integer]
nats = [1..]
However, I would love to be able to opt in to declaring functions total on a case-by-case basis, like Idris can.
> This fine, though, because for ordinary programming, a proof of totality isn't a useful guarantee. You care how long programs actually take to run, not whether they would theoretically finish eventually.
This wouldn't be the point of the guarantee for me. Haskell functions already give you assurances that you've not made any mistakes:
* You haven't accidentally introduced null, or missed any null checks.
* You haven't written code which will do a different thing tomorrow than it did today.
* Your function won't race, nor will it cause other functions to race.
If you have a function Foo->Bar, and you give it a Foo, you've all-but-proved that you'll get a valid Bar back. How can you screw that up? By diverging. I'm not trying to put a bound on a long-running function, I just want the type system to make sure the function isn't sucking on its own tailpipe.
Yes, it would detect a certain class of mistakes where you put an infinite loop or infinite recursion in your code. But I find these are pretty rare, and there would still be other mistakes where on some inputs, it would take a year to run.
It's only when proving theorems that a mathematical proof of totality matters, and there are specialized languages for that.
For most people, we test in order to make a scientific claim, that we tried running it, and it worked for the inputs we tried, and completed in a reasonable amount of time.
This is true of property testing and even model-checking; in simple cases, sometimes an exhaustive test can be done, but they don't actually prove statements outside the bounds used when testing.