> "I guarantee that if you send me an int then i will return you an int without crashing"
This is a much stronger guarantee than you get in any language except very specialized ones. Coq, for example (not just not crashing, but also guaranteed termination). But even in Haskell an Int -> Int function can crash or decide not to terminate. Reading more into a type opens up cans of worms that are hard to solve.
The only no_returns otherwise are loops and hibernates. Hibernates are explicit. You might have a hard time analyzing the tail-calls to figure out an ultimate type that captures a no_return loop, but I think ignoring that condition would not be horrible for a BEAM type system (along the same lines as the random number crash scenario that I described).
I'm not sure what you're saying. Crashing "miscodes" (like pattern match failures) are a thing, no? A "well defined" thing, but not one that a type system that doesn't include proper theorem proving will save you from.
An effects tracking system can be used to determine things such as use of FFI, `assert`, recursion, and side effects. With these statements like "this function does not crash" is easy, and "this function does not diverge" is also possible, though it will not detect all functions that do not diverge.
Most languages don't have a way to type that, I'm pretty sure it requires dependent types.
The types don't prove the logic doing the right thing or that nothing can break while the function runs, but they prove that you are using it mostly correctly in what you give it and what you do with what it'll return.
let's go with a simpler one: int -> int
"I guarantee that if you send me an int then i will return you an int without crashing"
In elixirland: `IO.inspect/1` would satisfy this, as would `Kernel.-/1`. The interesting thing is that `any -> int` is then a subtype of `int -> int` and we need a new type `_ -> int` which is "any one-arity function that emits int".
Then types become a statement of "resistance to crashing" in the BEAM vm, which I think is the useful thing that people are looking for.
I don't have answers to everything; I don't know how to deal with a function that generates random numbers from 1 to 20 and crashes on 13, for example.
We should have a discussion about this! I'll reach out on another channel.