3 ms·
> I don't want to stick linear or dependent types into TLA+. Proving dynamic properties with an exhaustive runtime is a totally different game from what you mig
by erichocean 1mo ago
> I don't want to stick linear or dependent types into TLA+. Proving dynamic properties with an exhaustive runtime is a totally different game from what you might do statically.
Yup, TLA+ is a totally different beast from, say, Lean 4. Both are useful. I don't want dependent types in TLA+ either.