4 ms·

How valuable is TLA+ for non-concurrent applications? I've always been interested in formal verification (is TLA+ technically that?).

colonelcanoe 6y ago
You can construct formal proofs about a TLA+ spec, using the "TLA proof system" (TLAPS). Or, you can verify properties for "bounded models" of your spec via brute force. The latter is much less overhead, so it's good to use bounded models (with the TLC model checker) to become confident in the spec, then construct proofs if warranted.
Taikonerd 6y ago
> How valuable is TLA+ for non-concurrent applications? My understanding is that TLA+ is for concurrent applications, but with a broad definition of "concurrent." For example, it could be... * multiple hosts messaging each other * multiple threads in one process sharing a data structure * multiple API calls that all use the same Postgres DB In other words, any sort of system where different actors can step on each others' toes.
- Jtsummers 6y ago
  That's definitely the main use. But TLA+ can also be applied to single threaded specifications by encoding various invariants (pre/post conditions on entry and exit, loop invariants).
- flazzarino 6y ago
  You define variables and code that changes the variables over time. TLA+ lets you observe variable states and assert constraints. The amount of concurrency is up to you, it works fine with a single process. Non-determinism might be a better thing to anchor the value to. For example in a deterministic "normal" programming environment, an if/then/else statement will execute only one out of two possible code paths. You have to run the code with a complementary condition to observe the other code path. In a non-deterministic environment like TLA+ both possible code paths are executed. You can observe state transitions in both possibilities. In a deterministic context the combinatorics of code paths can get out of hand quickly. Non-deterministically you have one set of assertions for all code paths, or patterns of paths.
hwayne 6y ago
If you don't have any concurrency or nondeterminism in your spec, then you'll probably want different tools. It's not that TLA+ is bad at modeling single-threaded algorithms, it's just that makes a lot of design decisions around representing concurrency, and there's an opportunity cost to that. I'd consider a code-level formal verification language, like Liquid Haskell or Dafny.

colonelcanoe 6y ago

You can construct formal proofs about a TLA+ spec, using the "TLA proof system" (TLAPS). Or, you can verify properties for "bounded models" of your spec via brute force. The latter is much less overhead, so it's good to use bounded models (with the TLC model checker) to become confident in the spec, then construct proofs if warranted.

Taikonerd 6y ago

> How valuable is TLA+ for non-concurrent applications? My understanding is that TLA+ is for concurrent applications, but with a broad definition of "concurrent." For example, it could be... * multiple hosts messaging each other * multiple threads in one process sharing a data structure * multiple API calls that all use the same Postgres DB In other words, any sort of system where different actors can step on each others' toes.

Jtsummers 6y ago
That's definitely the main use. But TLA+ can also be applied to single threaded specifications by encoding various invariants (pre/post conditions on entry and exit, loop invariants).
flazzarino 6y ago
You define variables and code that changes the variables over time. TLA+ lets you observe variable states and assert constraints. The amount of concurrency is up to you, it works fine with a single process. Non-determinism might be a better thing to anchor the value to. For example in a deterministic "normal" programming environment, an if/then/else statement will execute only one out of two possible code paths. You have to run the code with a complementary condition to observe the other code path. In a non-deterministic environment like TLA+ both possible code paths are executed. You can observe state transitions in both possibilities. In a deterministic context the combinatorics of code paths can get out of hand quickly. Non-deterministically you have one set of assertions for all code paths, or patterns of paths.

hwayne 6y ago

If you don't have any concurrency or nondeterminism in your spec, then you'll probably want different tools. It's not that TLA+ is bad at modeling single-threaded algorithms, it's just that makes a lot of design decisions around representing concurrency, and there's an opportunity cost to that. I'd consider a code-level formal verification language, like Liquid Haskell or Dafny.