Comment by nylonstrung
4 hours ago
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.
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"?