alt Hacker News>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?
I would expect it to require a proof that 1 - 2 is non-negative. That's kind of the raison d'etre of Lean isn't it?
The reason they don't do that is because Lean treats proofs as manually generated explicit objects, unlike other languages like Dafny (IIRC) where they are implicit. Requiring explicit proofs for every subtraction was presumably seen as too onerous.
Which is fine... BUT they then should have said "so we're going to define a more convenient operator which is LIKE subtraction but isn't actually standard subtraction, and therefore we won't use the standard subtraction notation for it".
If they had used something like 1 -_ 2 then that would be much less surprising because you'd think "oh right, it's the special saturating subtraction".
Similarly for Uint8.ofNat it should have been Uint8.ofNatWrapping or similar.
This shouldn't be news.