3 ms·

There are two pieces of TLA+ and formal modeling that I don't get. (And I'm pretty sure all the authors and documenters have tried their best at explaining it a

There are two pieces of TLA+ and formal modeling that I don't get. (And I'm pretty sure all the authors and documenters have tried their best at explaining it again and again, but maybe asking the question again is not useless.) 1. Given you have to learn the language, and, at first, you don't know it - how do you even trust that you're writing a proof right, and that you're not simply writing gibberish ? TDD has code execution as an "arbiter of peace". If, when calling a function, you get an unexpected result, then... you did something wrong. If my TLA+ set of rules holds, how do I get confidence that I wrote the right set of rules ? 2. Once I've got a set of rule that I decided to trust, when I implement it and I get bugs (as demonstrated by executable code) ; how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ? Maybe it becomes obvious once you've done it, and I'm sorry to be the million'th to say such nonsense. Sorry.

deleted 6y ago
[deleted]
fpgaminer 6y ago
TLA+ is fear driven development. If you have any fears that your TLA+ model or proofs might have been written wrong, your job is to encode those fears as further TLA+ proofs. The last TLA+ specification I wrote was only about two pages long. The actual model was a handful of lines. A handful of definitions. And then a page and a half of proofs and proof proofs. So it's easy to look over your spec exhaustively. And if there's any part of it you aren't sure about, or think you might have written wrong, then write more proofs that show that it you can't have written it wrong that way. The IDE provides lots of feedback and ways to debug. So like learning any language, you'll spend your formative time just trying out different parts of the TLA+ semantics and introspecting the outputs to make sure the models are behaving the way you expect them to. TLA+ is very much like doing math. If you do it wrong, you get answers that don't make sense. And it's easy to check if you're doing it wrong, by doing something you _know_ is wrong. If you get a "right" answer, you know you are making a mistake or don't understand a semantic correctly. The joy is that TLA+ allows you to write out these proof proofs and have them checked every time along with the rest of your spec. > how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ? Your implementation and your TLA+ model share the same state data structures (though the TLA+ model might have a simplified representation of those states, eliding unimportant details). If you suspect your spec, you just copy the broken state sequence your implementation is encountering into your TLA+ model. If the model displays the same behavior you know your spec is wrong. If it doesn't, you know your implementation is wrong.
Jtsummers 6y ago
TLA+ specs are often short which aids in verifying and validating them, especially in comparison to typical development projects. TLA+ also permits ignoring non-essential details and focusing on the core aspects of the problem. As an example of the latter, I used TLA+ once (only) for work to great success. But the spec I wrote ignored nearly every detail about the larger system, and focused on a few hardware details and modeled the shared memory system as a simple sequence of, rather arbitrarily, 5-11 elements (fixed in the models, in the spec it was a variable). What was stored in the memory? It didn't matter at all, it could literally be anything as far as the model and spec were concerned. My point being, the spec was so simple that visual inspection and a bit of analysis could tell us that it was correct, it fit in a couple pages if printed out. Model checking let us verify that it had the desired behaviors (with respect to the invariants that I put in based on the official specs for the hardware). Later, weakening the invariants allowed me to "recreate" the race condition that existed in the hardware implementation and was causing all our problems.
hwayne 6y ago
> 1. Given you have to learn the language, and, at first, you don't know it - how do you even trust that you're writing a proof right, and that you're not simply writing gibberish ? TDD has code execution as an "arbiter of peace". If, when calling a function, you get an unexpected result, then... you did something wrong. I write TLA+ specs in the same way I do TDD: first write an invariant or property I know I should half, then make it fail, then modify the spec to pass the invariant. > If my TLA+ set of rules holds, how do I get confidence that I wrote the right set of rules ? Ultimately, nothing can guarantee this for us, just as nothing can guarantee we wrote the right code. This is one reason why I'm a strong advocate of spec reviews. Getting another pair of eyes on the spec goes a long way. > 2. Once I've got a set of rule that I decided to trust, when I implement it and I get bugs (as demonstrated by executable code) ; how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ? It depends. This has happened to me a couple of times before. In one case, it was because I forgot to include something in the spec. Adding that caused the spec to immediately fail, which corresponded to the executable bug. In another case, I was able to identify, assuming the spec was correct, where the spec-code mistmatch must have been to cause the bug. So I was able to identify the code issue much faster than without the spec. It helps that specs are usually much smaller than the corresponding codebase, so you can sweep it for issues much faster.

deleted 6y ago

[deleted]

fpgaminer 6y ago

TLA+ is fear driven development. If you have any fears that your TLA+ model or proofs might have been written wrong, your job is to encode those fears as further TLA+ proofs. The last TLA+ specification I wrote was only about two pages long. The actual model was a handful of lines. A handful of definitions. And then a page and a half of proofs and proof proofs. So it's easy to look over your spec exhaustively. And if there's any part of it you aren't sure about, or think you might have written wrong, then write more proofs that show that it you can't have written it wrong that way. The IDE provides lots of feedback and ways to debug. So like learning any language, you'll spend your formative time just trying out different parts of the TLA+ semantics and introspecting the outputs to make sure the models are behaving the way you expect them to. TLA+ is very much like doing math. If you do it wrong, you get answers that don't make sense. And it's easy to check if you're doing it wrong, by doing something you _know_ is wrong. If you get a "right" answer, you know you are making a mistake or don't understand a semantic correctly. The joy is that TLA+ allows you to write out these proof proofs and have them checked every time along with the rest of your spec. > how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ? Your implementation and your TLA+ model share the same state data structures (though the TLA+ model might have a simplified representation of those states, eliding unimportant details). If you suspect your spec, you just copy the broken state sequence your implementation is encountering into your TLA+ model. If the model displays the same behavior you know your spec is wrong. If it doesn't, you know your implementation is wrong.

Jtsummers 6y ago

TLA+ specs are often short which aids in verifying and validating them, especially in comparison to typical development projects. TLA+ also permits ignoring non-essential details and focusing on the core aspects of the problem. As an example of the latter, I used TLA+ once (only) for work to great success. But the spec I wrote ignored nearly every detail about the larger system, and focused on a few hardware details and modeled the shared memory system as a simple sequence of, rather arbitrarily, 5-11 elements (fixed in the models, in the spec it was a variable). What was stored in the memory? It didn't matter at all, it could literally be anything as far as the model and spec were concerned. My point being, the spec was so simple that visual inspection and a bit of analysis could tell us that it was correct, it fit in a couple pages if printed out. Model checking let us verify that it had the desired behaviors (with respect to the invariants that I put in based on the official specs for the hardware). Later, weakening the invariants allowed me to "recreate" the race condition that existed in the hardware implementation and was causing all our problems.

hwayne 6y ago

> 1. Given you have to learn the language, and, at first, you don't know it - how do you even trust that you're writing a proof right, and that you're not simply writing gibberish ? TDD has code execution as an "arbiter of peace". If, when calling a function, you get an unexpected result, then... you did something wrong. I write TLA+ specs in the same way I do TDD: first write an invariant or property I know I should half, then make it fail, then modify the spec to pass the invariant. > If my TLA+ set of rules holds, how do I get confidence that I wrote the right set of rules ? Ultimately, nothing can guarantee this for us, just as nothing can guarantee we wrote the right code. This is one reason why I'm a strong advocate of spec reviews. Getting another pair of eyes on the spec goes a long way. > 2. Once I've got a set of rule that I decided to trust, when I implement it and I get bugs (as demonstrated by executable code) ; how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ? It depends. This has happened to me a couple of times before. In one case, it was because I forgot to include something in the spec. Adding that caused the spec to immediately fail, which corresponded to the executable bug. In another case, I was able to identify, assuming the spec was correct, where the spec-code mistmatch must have been to cause the bug. So I was able to identify the code issue much faster than without the spec. It helps that specs are usually much smaller than the corresponding codebase, so you can sweep it for issues much faster.