alt Hacker Newshow is lean different from tlaplus for helping you with reasoning during the design phase?
I literally just discovered tlaplus last week after struggling with reasoning about the explosion of permutations about configuration policies Im designing, and Im still learning the math but Im finding it easier to reason with tlaplus than in code is lean like that?
You can embed TLA+ into Lean. I don't think that there's any benefit to formalization before coding unless you're working on like million dollar projects