3 ms·

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 typ

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

jkhdigital 2mo ago
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.
- deterministic 2mo ago
  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. :)
inigyou 2mo ago
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"?
- samus 2mo ago
  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.
  - inigyou 2mo ago
    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.
- nylonstrung 2mo ago
  > 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.
noosphr 2mo ago
Lean is a dsl for mathematicians, not computer programmers.
- nylonstrung 2mo ago
  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
  - IsTom 2mo ago
    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).
    - nylonstrung 2mo ago
      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 https://github.com/leanprover-community/repl
      - IsTom 2mo ago
        Using JSON as input and output of a REPL is certainly a choice.
- deterministic 2mo ago
  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.

jkhdigital 2mo ago

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.

deterministic 2mo ago
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. :)

inigyou 2mo ago

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

samus 2mo ago
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.
- inigyou 2mo ago
  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.
nylonstrung 2mo ago
> 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.

noosphr 2mo ago

Lean is a dsl for mathematicians, not computer programmers.

nylonstrung 2mo ago
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
- IsTom 2mo ago
  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).
  - nylonstrung 2mo ago
    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 https://github.com/leanprover-community/repl
    - IsTom 2mo ago
      Using JSON as input and output of a REPL is certainly a choice.
deterministic 2mo ago
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.