4 ms·

What makes state hard to reason about mathematically? TLA+ has a very formal definition of state and time that can be model checked or used for proofs. I think

What makes state hard to reason about mathematically? TLA+ has a very formal definition of state and time that can be model checked or used for proofs. I think the reason that this is such a common statement is exactly because people don’t even know that state can be reasoned about mathematically, they just assume that it can’t be. The biggest thing that TLA+ showed me is that there’s no difference between functional and imperative programming from an algorithm standpoint. You can implement the exact same algorithm in both paradigms, and while the functional one has no explicit state, it can have a tremendous amount of implicit state. Recursion where a new state parameter is passed as argument to the next call is just as difficult to reason about as mutable state, it’s just less efficient from a processor standpoint.

bordercases 6y ago
I have no experience using TLA+, just secondhand knowledge, so you might very well be right. From my understanding, everything I said is true when restricted to classical logic. Otherwise, there are multiple approaches to objects and time, all of which are non-classical logics, and so are not commonly taught nor have they yet been embedded in many languages. TLA+ has been getting more traction, which might signal some kind of convergence since I last looked into it? I guess Rust would be another example where state is checked against using ownership signals, which uses non-classical concepts. Defending myself against the second claim, yes these algorithms have implicit state because the machines we're operating on are fundamentally stateful. But that's meant to be abstracted away at the language level and left for the interpreter/compiler to resolve. This still leaves problems for how to modularize code at the domain layer using functional idioms, which primarily express behavior over properties. OOP can be restricted in a way which makes this simple to bridge towards using the Actor model but that's still a step away from habitually structuring your code using modules monoids and combinators. TLA+ doesn't quite address this, since (IIRC) you don't implement your final system in TLA+.

bordercases 6y ago

I have no experience using TLA+, just secondhand knowledge, so you might very well be right. From my understanding, everything I said is true when restricted to classical logic. Otherwise, there are multiple approaches to objects and time, all of which are non-classical logics, and so are not commonly taught nor have they yet been embedded in many languages. TLA+ has been getting more traction, which might signal some kind of convergence since I last looked into it? I guess Rust would be another example where state is checked against using ownership signals, which uses non-classical concepts. Defending myself against the second claim, yes these algorithms have implicit state because the machines we're operating on are fundamentally stateful. But that's meant to be abstracted away at the language level and left for the interpreter/compiler to resolve. This still leaves problems for how to modularize code at the domain layer using functional idioms, which primarily express behavior over properties. OOP can be restricted in a way which makes this simple to bridge towards using the Actor model but that's still a step away from habitually structuring your code using modules monoids and combinators. TLA+ doesn't quite address this, since (IIRC) you don't implement your final system in TLA+.