|
These posts about how a type system can guarantee correctness always make me a little envious of the poster. Not envy that their work isn't hard, but that it has a kind of straightforwardness, with problems so well-defined that a proper analysis guarantees you've solved it completely. In my work, the types are usually so nailed-down there isn't any question about them. Yet the problems can be so nonlinear and ill-conditioned that even moderate testing-- say, hitting the code with 1000 test cases-- is just not enough to convince myself it's working correctly. It often happens that a unit test runs just fine at that level, but bumping it up to 10,000 or 100,000 cases reveals weaknesses in the code. Illustrative example follows-- no need to read if you "get" that, in some fields, a type system simply doesn't detect the interesting bugs. A few months ago, I was testing methods for solving problems of sorption to room surfaces. In terms of types, it could hardly get more explicit. Take an object representing a sorption isotherm, plus two double-precision numbers giving gas- and sorbed-phase concentrations, and return the equilibrium concentration at the sorbent surface. The only way to specify the types more completely would be to tag all the numbers involved with units. Guaranteeing convergence turned out to be a royal pain. To get a useful answer, you need to force convergence to very tight tolerances-- tight enough that, on ill-conditioned problems, you run the risk of asking for answers below the machine precision. That means you need two termination tests-- one on the defining equation (is the error close enough to zero?), and one on the returned result (is the current best answer within a tight enough bracket?). And within that framework, it's very easy to create algorithms that, due to finite-precision effects, fall into infinite loops because they fail to actually change a bracket point when they add a small number to it. So again, types were not an issue. The only way I was sure I had all the convergence pitfalls out of the way was extensive unit testing. And the baby tests I ran during initial development-- sampling 1000 combinations out of a database of sorbents and chemicals-- simply didn't do it. Once I had "working" code, and stepped up sampling to the 100,000 range, it was easy to discover oddball combinations that would cause problems. |
Why can't a type system keep track of units? Why can't it be aware of precision? If it's possible for you to find a proof that a particular implementation of your algorithm won't fall into an infinite loop, then there is a type system that can verify that your algorithm will terminate. Of course, actually designing a sound type system with this property could be quite tricky, and I have no idea what the resulting language would look like -- but it would be possible.