I disagree completely. Having runtime checks or not if the code that's written is basically randomly stringed together expressions, are all unsound code.
This is runtime type-checks:
if x == null: die "Nullpointer exception";
it is simply not better than:
x.DoTheThing();
They are equivalent.
The solution to that is not a runtime check, it's actually using a typing system in the first place. Runtime type-checks is no different from:
let x = 42;
if x != 42: die "It's supposed to be 42";
compute_the_thing x;
if x != 42: die "It's supposed to be 42";
save x;
if x != 42: die "It's supposed to be 42";
Only completely unsound code would rely on something like that.
I know that I'm not checking types in my pretend-o-code.
"In practice, if the car I ordered is a pizza, I want to know!"
I would say that this is misusing my analogy by flirting with simple value bugs. Ordering a thing and getting the wrong kind of product, that's perfectly understandable in the world of bugs and what not.
Calling the place_order function, expecting to get back an order object but instead getting the function "not" or a database connection, that's more akin to what we're talking about here. It's the wrong data type and having a runtime check to catch that is a sign of dealing with unsound code.
Just crash everything is what _you_ are suggesting because that failing runtime type-check _is_ a de facto runtime crash of whatever was running at that point.
Code that runs the risk of encountering such a problem should not compile because it's not even wrong.
This is runtime type-checks: if x == null: die "Nullpointer exception";
it is simply not better than: x.DoTheThing();
They are equivalent.
The solution to that is not a runtime check, it's actually using a typing system in the first place. Runtime type-checks is no different from:
let x = 42; if x != 42: die "It's supposed to be 42"; compute_the_thing x; if x != 42: die "It's supposed to be 42"; save x; if x != 42: die "It's supposed to be 42";
Only completely unsound code would rely on something like that.
I know that I'm not checking types in my pretend-o-code.
"In practice, if the car I ordered is a pizza, I want to know!"
I would say that this is misusing my analogy by flirting with simple value bugs. Ordering a thing and getting the wrong kind of product, that's perfectly understandable in the world of bugs and what not.
Calling the place_order function, expecting to get back an order object but instead getting the function "not" or a database connection, that's more akin to what we're talking about here. It's the wrong data type and having a runtime check to catch that is a sign of dealing with unsound code.
Just crash everything is what _you_ are suggesting because that failing runtime type-check _is_ a de facto runtime crash of whatever was running at that point.
Code that runs the risk of encountering such a problem should not compile because it's not even wrong.