> In an ideal world, tests would be subsumed by types
It would be literally impossible for this to happen in a Turing-complete language, though, because a hypothetical 'perfect' type system would be able to solve the halting problem.
(Essentially, Bottom is a member of every type, or else the compiler would need to distinguish between a halting program and a non-halting program before accepting the input program).
Some people argue that in an ideal world we wouldn't be using Turing-complete languages. Nothing like a total functional programming language to make life better :).
I thought about total functional programming, like Agda. But even if you have Turing completeness, you can add time constraints to tests and everything will be decidable.
It would be literally impossible for this to happen in a Turing-complete language, though, because a hypothetical 'perfect' type system would be able to solve the halting problem.
The Haskell 'Bottom' type alludes to this in its documentation, actually: http://www.haskell.org/haskellwiki/Bottom
(Essentially, Bottom is a member of every type, or else the compiler would need to distinguish between a halting program and a non-halting program before accepting the input program).