> this is definitely not a bad one
It definitely is a bad convention because it's highly surprising. That's what makes it a footgun.
> that would be a really annoying thing to use
Sure. So maybe provide "unchecked" versions for when people don't want to bother.
We've known this about interface design for literally decades. The default must be safe and unsurprising. You need to opt into unsafety.
>It definitely is a bad convention because it's highly surprising.
You know that `Nat` represents non-negative numbers, and you see that `1 - 2` does not produce a compile error. What value do you expect then? What’s so surprising about choosing zero as a default value here? Do you expect it to panic or what?