3 ms·

I have no skin in this game, but: > "I guarantee that if you send me an int then i will return you an int without crashing" This is a much stronger guarantee

I have no skin in this game, but: > "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.

lpil 6y ago
I think you can usefully tackle this problem without too much difficulty. At least, within a langauge like Gleam you can. 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.
dnautics 6y ago
Ok so aside from well known out of control things like another process telling the vm to brutal_kill you, cosmic arrays, or miscodes, OS interactions, oom errors or nif panics (the last three which bring down the whole VM anyways, so who cares), the crashing surface error for a BEAM process is extremely well defined. 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).
- tom_mellior 6y ago
  > Ok so aside from well known out of control things like another process telling the vm to brutal_kill you, cosmic arrays, or miscodes [...] the crashing surface error for a BEAM process is extremely well defined. 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.

lpil 6y ago

I think you can usefully tackle this problem without too much difficulty. At least, within a langauge like Gleam you can. 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.

dnautics 6y ago

Ok so aside from well known out of control things like another process telling the vm to brutal_kill you, cosmic arrays, or miscodes, OS interactions, oom errors or nif panics (the last three which bring down the whole VM anyways, so who cares), the crashing surface error for a BEAM process is extremely well defined. 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).

tom_mellior 6y ago
> Ok so aside from well known out of control things like another process telling the vm to brutal_kill you, cosmic arrays, or miscodes [...] the crashing surface error for a BEAM process is extremely well defined. 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.