Hacker News Reader

Comment by nylonstrung | Hacker News Reader

This is valid and my take is that domain modelling becomes extremely important in this context

More then theorem proving what attracts to Lean is that it's type system is insanely powerful, indexed dependant inductive and quotient types allow the realization of "making invalid states unrepresentable" to a degree no other language can, except perhaps a custom DSL built with Racket

One must remember that Lean wasn't made for math, it ended up succeeding in that vertical because it was expressive enough to represent the extensive design space mathematicians were dealing with

And I think that's equally applicable to specs and business logic

View on HN

Yeah I feel like the hype around “formal methods” is really just a growing interest in expressive type systems that enable more and more program semantics to be declared in code rather than in comments. Correctness is good, but so are portability and modularity and extensibility.

LEAN is exactly an expressive type system. Nothing more. The amazing thing is that the type system is so powerful that you can express cutting-edge mathematics with it and prove it correct.

In other words, proving something is essentially the same thing as type checking.

It absolutely blew my mind when I finally understood how it works. For that reason alone, LEAN is worth diving into. :)

Is a type like "fixed-size list of 3 integers" really more useful than a type like "list of integers" plus a constraint "size must be 3"? I feel like the latter is more flexible. Does Lean have a type for "list containing only prime powers"?

To some degree these are the same things, depending on the type system. But it might be easier to write a function accepting a list of size 3 than matching on a constraint, which might get separated from the variable it annotates.

The difference is that (generally in programming languages) a type is something defined with a name while a constraint is ad-hoc. If you use types for everything you'll have to write a whole lot: this variable is a Size3List, this one is a Size5List, this one is a PrimePowersList.

> Does Lean have a type for "list containing only prime powers"?

You can wrap a base type with a proof which is called bundling

inductive PrimePower where | mk (n : Nat) (prf : IsPrimePower n)

So in this case the type checker will not allow construction unless the proof demonstrates they are prime powers

The prf part gets erased at runtime so there's no overhead. You could also use a constraint/refinement type like you talked about and it's more flexible as it relates to using list operations like map filter reverse etc.

Lean is a dsl for mathematicians, not computer programmers.

This is not remotely true, it was designed as a general purpose functional programming language and the adoption by mathematicians only came later with the creation of Mathlib.

It's not a DSL but has very powerful metaprogramming capabilities that make it great for creating DSLs

There's nothing the core language lacks compared to say Haskell

I wish DX was better for people not using VS. I have my opinions about tools and when trying lean out I got the impression that you basically have to use it. They also seemingly lack a REPL.

I also got the impression that they like sticking everything into Mathlib and not splitting off smaller packages that you could use as dependencies (besides Batteries).

Yeah I really dislike that you need neovim or VS to benefit from Infoview

Haven't tried it but there's this community-made REPL https://github.com/leanprover-community/repl

Using JSON as input and output of a REPL is certainly a choice.

Completely and 100% utterly wrong. LEAN is a functional programming language with a type system strong enough to express cutting-edge mathematics and proving it correct. And yes it also has DSL's built on top of it optimised for doing math but that is an extra.

Reply on news.ycombinator.com