[thomasmg]

> the only feasible compiler solutions to preventing division-by-0 errors are either: defining the behaviour, which always ends up surprising people later on, or; incredibly cumbersome or underperformant type systems/analyses which ensure that denominators are never 0.

I don't think it's very cumbersome if the compiler checks if the divisor could be zero. Some programming languages (Kotlin, Swift, Rust, Typescript...) already do something similar for possible null pointer access: they require that you add a check "if s == null" before the access. The same can be done for division (and remainder / modulo). In my own programming language, this is what I do: you can not have a division by zero at runtime, because the compiler does not allow it [1]. In my experience, integer division by a variable is not all that common in reality. (And floating point division does not panic, and integer division by a non-zero constant doesn't panic either). If needed, one could use a static function that returns 0 or panics or whatever is best.

[1] https://github.com/thomasmueller/bau-lang/blob/main/README.m...

[ivanbakel]

>Some programming languages (Kotlin, Swift, Rust, Typescript...) already do something similar for possible null pointer access: they require that you add a check "if s == null" before the access.

For Rust, this is not accurate (though I don't know for the other languages). The type system instead simply enforces that pointers are non-null, and no checks are necessary. Such a check appears if the programmer opts in to the nullable pointer type.

The comparison between pointers and integers is not a sensible one, since it's easy to stay in the world of non-null pointers once you start there. There's no equivalent ergonomics for the type of non-zero integers, since you have to forbid many operations that can produce 0 even on non-0 inputs (or onerously check that they never yield 0 at runtime).

>The same can be done for division (and remainder / modulo). In my own programming language, this is what I do: you can not have a division by zero at runtime, because the compiler does not allow it... In my experience, integer division by a variable is not all that common in reality

That's another option, but I hardly find it a real solution, since it involves the programmer inserting a lot of boilerplate to handle a case that might actually never come up in most code, and where a panic would often be totally fine.

Coming back to the actual article, this is where an effect system would be quite useful: programmers who actually want to have their code be panic-free, and who therefore want or need to insert these checks, can mark their code as lacking the panic effect. But I think it's fine for division to be exposed as a panicking operation by default, since it's expected and not so annoying to use.

[thomasmg]

The syntax in Kotin is: "val name: String? = getName(); if (name != null) { println(name.length) // safe: compiler knows it's not null }" So, there is no explicit type conversion needed.

I'm arguing for integer / and %, there is no need for an explicit "non-zero integer" type: the divisor is just an integer, and the compiler need to have a prove that the value is not zero. For places where panic is fine, there could be a method that explicitly panics in case of zero.

I agree an annotation / effect system would be useful, where you can mark sections of the code "panic-free" or "safe" in some sense. But "safe" has many flavors: array-out-of-bounds, division by zero, stack overflow, out-of-memory, endless loop. Ada SPARK allows to prove absence of runtime errors using "pragma annotate". Also Dafny, Lean have similar features (in Lean you can give a prove).

> I think it's fine for division to be exposed as a panicking operation by default

That might be true. I think division (by non-constants) is not very common, but it would be good to analyze this in more detail, maybe by analyzing a large codebase... Division by zero does cause issues sometimes, and so the question is, how much of a problem is it if you disallow unchecked division, versus the problems if you don't check.