6 ms·
That is more than just your intuition--with minor tweaking, it is a theorem that was taught in my Programming Language Theory course when I was in college! The
by gliese1337 7y ago
That is more than just your intuition--with minor tweaking, it is a theorem that was taught in my Programming Language Theory course when I was in college!
The tweak is that any safe type system will preclude programs that are otherwise semantically valid. You can have a type system that catches some errors and lets others through, or you can have a type system that catches all errors but also excludes some valid formulas (or even, and most commonly, a type system that catches most errors, also prohibits some valid formulas, but nevertheless still lets other errors through), but you can't have a decidable type system that permits all semantically valid programs and excludes all erroneous programs.
- hinkley 7y agoIt’s also a multidimensional problem, so sometimes people improve the state of the art in one dimension, but either at the expense or the neglect of another. I think it’s a bit like any applied science. There’s a theoretical limit to the efficiency of an internal combustion engine. We grow closer to it, often with more complicated machinery, occasionally with better construction (ie, the manufacturing becomes more complex so the product is less complex). And we balance the consequences (pollution, reliability, cost) against the benefits. Once in a while we substitute a different model (E.g., Atkinson) with small but important differences in the theoretical limits, by looking at the problem differently.