I only see this now. Good reply. All valid concerns. But
> "I want all runtime errors to be at least this surprising", that level will be easier to achieve via types than via tests
For the type of the values, yes, but you still need tests for the content of the values. E.g you can only index into arrays with integers, but can your code access the array out of bounds? So that level is implicitly achieved.
> but the trouble is that code that's 95% typechecked might as well be 0% typechecked
That is absolutely not my experience. Typed at module boundaries really helps, even is that is only 5% of the code. On the other hand, getting to 100% type checked can be hard in current gradual systems. Mostly because some code is hard to type, even though it works fine, and humans can reason about it fine. Though you might be right, it is probably better expressed in a more type sound way. (Unless it is parametrization on function arity that does you in, grr.)
But to me, unless you are coding in idris or such, types are like the derivative of your code. Yes they show the general "slope"; how it fits together. But it says nothing on the values that flow through it, or the correctness of the code. You still need tests, and the type checker is not much more than a spell checker. Its usefulness is not in dispute (though overestimated by some). Just that in most of todays popular languages, you pay a price that is not non trivial. The choice is a tradeoff.
> For the type of the values, yes, but you still need tests for the content of the values. E.g you can only index into arrays with integers, but can your code access the array out of bounds? So that level is implicitly achieved.
So you create a path-dependent type for valid indices into a given array (or, more likely, use a safe way of expressing iteration so that you don't need to see indices directly). Yes you can check that your indexing is valid with tests, but it's more efficient to do it with types.
> That is absolutely not my experience. Typed at module boundaries really helps, even is that is only 5% of the code.
Maybe if they're enforced at those boundaries - does that happen? I'm thinking mainly of gradual typecheckers that are erased at runtime, which IME are useless, because a type error can easily propagate a long way before it's actually picked up, and you see an "impossible" error where something has a different type at runtime to its declared type.
> But to me, unless you are coding in idris or such, types are like the derivative of your code. Yes they show the general "slope"; how it fits together. But it says nothing on the values that flow through it, or the correctness of the code.
Not my experience once you get used to working with the type system. Anything that should always be true in a given part of the code, you make into part of the types. Make the types detailed enough that a function with a given signature can only have one possible meaning, and then any implementation of that function that typechecks must be correct.
> "I want all runtime errors to be at least this surprising", that level will be easier to achieve via types than via tests
For the type of the values, yes, but you still need tests for the content of the values. E.g you can only index into arrays with integers, but can your code access the array out of bounds? So that level is implicitly achieved.
> but the trouble is that code that's 95% typechecked might as well be 0% typechecked
That is absolutely not my experience. Typed at module boundaries really helps, even is that is only 5% of the code. On the other hand, getting to 100% type checked can be hard in current gradual systems. Mostly because some code is hard to type, even though it works fine, and humans can reason about it fine. Though you might be right, it is probably better expressed in a more type sound way. (Unless it is parametrization on function arity that does you in, grr.)
But to me, unless you are coding in idris or such, types are like the derivative of your code. Yes they show the general "slope"; how it fits together. But it says nothing on the values that flow through it, or the correctness of the code. You still need tests, and the type checker is not much more than a spell checker. Its usefulness is not in dispute (though overestimated by some). Just that in most of todays popular languages, you pay a price that is not non trivial. The choice is a tradeoff.