alt Hacker NewsThe thing I found really surprising about Lean is that although it is really focused on proving stuff, it has some surprisingly enormous footguns. What do you think the result of these are?
#eval (UInt8.ofNat 256 : UInt8)
#eval (4 - 5 : Nat)
Nope! Both give 0.
Replies
These are both pretty reasonable semantics for these functions. `UInt8.ofNat : Nat -> UInt8` might reasonably map the infinite number of `Nat` values to `UInt8` by taking the natural number modulo 256. And it's sensible enough that subtraction with natural numbers should saturate at 0.
These aren't the only reasonable semantics, and Lean will certainly let you define (for instance) a subtraction function on natural numbers that requires that the first argument is greater than or equal to the second argument, and fail at compile time if you don't provide a proof of this. These semantics do have the benefit of being total, and avoiding having to introduce additional proofs or deal with modeling errors with an `Except` type.
Good point, and an important example why static types are ultimately a failure: Encoding the actual invariants in them you care about is a pain in the ass.
No doubt there will be plenty of comments to your comment trying to rationalise this.
Who said that it should be a compile time error? That’s just a convention, and this is definitely not a bad one. No one is going to like the need to pass each time a proof that `a ≥ b` for every `a - b` invocation. Taking into account that this proof will most likely be an implicit argument, that would be a really annoying thing to use.
On the other hand, array indices by default do require such a proof, i.e., this code produces a compile time error:
Kevin Buzzard even wrote a blog post about a similar question about division by zero: https://xenaproject.wordpress.com/2020/07/05/division-by-zer...