[IshKebab]

The 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)

The first should be a compile time error right, because `UInt8.ofNat` is going to require that its argument is 0-255. And the second should be a compile time error because subtraction should not give a `Nat` unless the first argument is definitely more than the second.

Nope! Both give 0.

[unexpectedtrap]

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:

  def x := #[1, 2, 3, 4]
  #check x[7]

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...

[IshKebab]

> 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.

[unexpectedtrap]

>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?

[IshKebab]

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.

[unexpectedtrap]

>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 is to be able to write mathematical proofs, including proofs about your code, but not to attach proofs to every single function. This definition of subtraction does not prevent you from reasoning about it and requiring `a ≥ b` in the proofs/code for which this is really important.

>Requiring explicit proofs for every subtraction was presumably seen as too onerous.

Lean can deduce proofs implicitly as well. It’s just not a very reliable mechanism. That is, imagine your code breaking after an update, because Lean suddenly can’t deduce `a ≥ b` automatically for you anymore.

>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".

What is a standard subtraction over natural numbers at all? As you know, under a standard addition natural numbers form a monoid but not a group.

[IshKebab]

> Lean can deduce proofs implicitly as well.

Sure, but you still have to explicitly ask it to.

> What is a standard subtraction over natural numbers at all?

If you need something that is always defined then you have to use a non-standard subtraction (i.e. saturating subtraction). In other words the `-` operator should not work for Nat. It should require you to use `-_`.

[yuppiemephisto]

i agree about this point, i think this is one of the ways extensible syntax can save (or damn, like in this case) you

[JuniperMesos]

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.

[auggierose]

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.

[ux266478]

Why do you believe that static types are ultimately a failure?

[IshKebab]

I strongly disagree. Static types are a huge success. The problem here is essentially that they named things badly.

[JuniperMesos]

Better than simply not encoding the actual invariants you care about.