|
|
|
|
|
|
by logicchains
6 days ago
|
|
|
Lean's mostly used for maths, and tactics are much more ergonomic there. For writing correct-by-construction software programs, complex dependently-typed objects can be more ergonomic, as they allow passing a bunch of invariants through a program that are correct by construction, rather than needing to prove them at every stage via tactics. |
|
|