As the quote goes, dynamic typing is the belief that you can't explain to a computer why your code works, but you can keep track of it all in your head. If it's really hard to express in a given language then that's a problem with that language, but IME anything that's hard to express in statically-typed languages in general is a bad idea.
> And paying this penalty at API level, where ever user has to pay, is just a sin.
I'd say the opposite, because it's easy to cast away types when you don't need them, but it's virtually impossible to put type information back into a language that doesn't have it.
> The test suite idea was incorrect. Even 100% code coverage will not do. But for "normal" code, add reasonable amount of coverage. And any production runtime type error will be really surprising.
IME: For any given level of "I want all runtime errors to be at least this surprising", that level will be easier to achieve via types than via tests.
> A personal feeling on this topic is that it is all tradeoffs. But it makes me really happy to see gradual typing gaining traction. So you can start on your offroad bike, but end on a well oiled train, where that is worth the tradeoff. So you don't have to choose up front
IME it's ineffective - I spent years trying to get types working after the fact, but the trouble is that code that's 95% typechecked might as well be 0% typechecked. Every violation of typesafety needs to be visible right at the point where it happens if you're going to have any hope of correct code.
> Perhaps when we can even get runtime guarantees on perf/object layout when the type checker is happy.
That'd be nice. But it's going to take more advanced typing, not yes.
> "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.
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.