Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A perfectable programming language

alok.github.io

Post reply on HN
Print view View original

41–50 of 152 posts

Re: A perfectable programming language

#41

Post by unexpectedtrap »

IshKebab wrote: post #39

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 subtra…

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

Re: A perfectable programming language

#42

Post by senko »

c0balt wrote: post #27
unexpectedtrap wrote: post #19

Unfortunately Lean’s distribution went from somewhat about 15 MiB in times of Lean 3 to more than 2,5 GiB when unpacked nowadays for no good reason. This is too much. Even v4.0.0-m1 was a 90 MB archive. Looks like that Lean’s authors do not care about this anymore. Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad. Personally, I…

Lean is far off the most bloated one. Isabelle most likely takes that spot, the main archive includes a whole vscodium among other things.

>> Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three.

> Lean is far off the most bloated one. Isabelle most likely takes that spot.

Among these three is the operative phrase here.

I hate to be pedantic, but we are talking about theorem provers here :)

Re: A perfectable programming language

#44

Post by andai »

> For Eliza Zhang, who bet I couldn’t write a web app in C in one week using only the standard library. She was right. I didn’t know what any of those words meant. But I said the fuck I can’t, and that’s how I got into coding.

Re: A perfectable programming language

#45

Post by pjmlp »

unexpectedtrap wrote: post #19

Unfortunately Lean’s distribution went from somewhat about 15 MiB in times of Lean 3 to more than 2,5 GiB when unpacked nowadays for no good reason. This is too much. Even v4.0.0-m1 was a 90 MB archive. Looks like that Lean’s authors do not care about this anymore. Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad. Personally, I…

Static linking wonders?

Originally Lean was coded in C++, and dynamically linked executable, if I remeber correctly.

Re: A perfectable programming language

#46

Post by JuniperMesos »

IshKebab wrote: post #39

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 subtra…

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.

Re: A perfectable programming language

#48

Post by vouwfietsman »

shevy-java wrote: post #32

> languages without types tend to grow them, like PHP in 7.4 and Python type annotations Well ... that is a trend that is driven largely by people who love types. Not everyone shares that opinion. See ruby. It is very hard to try to argue with people who love types. They will always focus on "types are great, every language must have them". They, in general, do not acknowledge trade-offs when it comes to type systems…

> do not acknowledge trade-offs when it comes to type systems

Could you elaborate?

Re: A perfectable programming language

#49

Post by lelanthran »

shevy-java wrote: post #32

> languages without types tend to grow them, like PHP in 7.4 and Python type annotations Well ... that is a trend that is driven largely by people who love types. Not everyone shares that opinion. See ruby. It is very hard to try to argue with people who love types. They will always focus on "types are great, every language must have them". They, in general, do not acknowledge trade-offs when it comes to type systems…

> > languages without types tend to grow them, like PHP in 7.4 and Python type annotations

...

> Not everyone shares that opinion. See ruby.

All programming languages that have values (i.e. all of them) have types, because you cannot have a concrete value that doesn't have a type. This includes Ruby.

The only difference is whether the language lets you annotate the source code with the expected type of each value.

This is why you observe that all languages trend towards visible typing: The types are already there and it's only a matter of whether the language lets the programmer see it, or lets a linter enforce it, and everyone likes linters.

> So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types.

Maybe you misidentified where the type declaration is coming from? It might not be coming from people who want to see types in the source code, it most probably is coming from people who want a decent linter.

In 2026, programming without type-enforcement is like programming using an LLM; it's quicker, but less safe.

Re: A perfectable programming language

#50

Post by auggierose »

IshKebab wrote: post #39

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 subtra…

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.

Post reply on HN