Languages in the Dependent ML family allow users to ensure termination by using a termination metric, a number that is strictly decreasing on recursive calls in the definition of the function.
There is a counterpart to termination for co-recursive structures, where we need to show that a function produces values indefinitely. So, for the Collatz conjecture, we want to show termination for:
collatz n = collatz' n  collatz' 1 r = 1:r collatz' n r = if n `mod` 2 == 0 then collatz' (n `div` 2) (n:r) else collatz' (3*n + 1) (n:r)But for the twin prime conjecture we want to show the productivity of:
data Stream a = Stream a (Stream a) twins = twins' 3 twins' n = if (primep n) && (primep (n+2)) then Stream (n,n+2) (twins' (n+2)) else twins (n+2)
I don't know if any of the members of the DML family can check productivity. Imagine they could, and imagine we had a non-constructive proof of the twin primes conjecture. Could we use that proof to allow a definition of
twins to be marked productive?
Most of the time, we talk about the Curry-Howard correspondence in reference to intuitionist logic and functional programming, but non-constructive proofs of productivity seem like a good way to be able to use more powerful logic in programming, since they don't have to change the implementation of the function they are attached to.