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