3 ms·

You won't use this to model your web application, but the core logic. Usually it's really important that this core logic doesn't break. Imagine something lik

You won't use this to model your web application, but the core logic. Usually it's really important that this core logic doesn't break. Imagine something like twitter, why would you model it? Once you start thinking of having N servers, and you have to deal with caches, and consistence of message then it might make sense to model it to make sure that tweets get to the right users, are not lost and duplicates don't happen. You are not exactly modeling the web or mobile application but the "system". At the end of the day, your goal is a logically sound system. So figure out what will make your web application non-logically, if it's going to provide a terrible experience and it's hard to reason, then you might want to model it.

heavenlyblue 8y ago
OK, but could you model Twitter in TLA+ and then would TLA+ be able to find inconsistencies in the model given that you relax certain assumptions? Can TLA+ direct you to which of the caches is being incorrectly invalidated given that you have provided that 10% of the servers online are still using the old version of the software? That seems interesting, but haven't yet played with TLA+ enough to know that.
- pron 8y ago
  You can't know which of the caches is incorrectly validated, but if you specify the behavior of both new and old versions, you could check to see if mixing them could cause problems. But the more elaborate the specification, the harder it may be to answer the question. Using tools like Coq, you essentially need to write the proof (say, of the claim that mixing the versions could cause no issue with data consistency) yourself. With TLA+ you can do the same, but also have the option of letting the model checker check the theorem automatically for you, but the more elaborate the spec, the longer that would take. This is why you need to learn to specify at a level of detail that's right for answering the questions you want answered -- no lower (higher abstraction), or there may not be sufficient detail to answer them, and no lower, or answering may take a long time. Sometimes you'll find that you're specifying the same system at several levels of detail. One of the cool things in TLA+ is that you can check that the different levels are indeed related (could be a description of the same system at different levels).
  - heavenlyblue 8y ago
    On a more practical side of things - how do you mix your application code with TLA+? E.G. Do you have a "proof" project and a the code in different directories with comments in the TLA+ pointing to the files in the actual code? It would be incredibly nice if I could put TLA+ proofs in the comments next to every function or module I am working with and then choosing which of them to be proved. But that seems to be way beyond what the toolset allows you to do.
    - pron 8y ago
      1. Writing formal proofs in TLA+ (or in any other proof assistant) is almost always a waste of time. If the proof is very easy, you can certainly do it, but then you don't need to unless it's a strict requirement or an academic project whose entire purpose is to show that a formal proof is possible rather than some functional correctness requirement. And if the proof is not easy, then there are better methods, like using TLA+'s model checker. 2. Putting references to the TLA+ spec in the code could be nice and useful. 3. You should realize that the benefit from a powerful tool like TLA+ comes when it helps you reason about things that are hard for you to do, and those are hardly ever at the code level. So while using a code-level tool like Why3 to prove some routine is cool, it is hardly ever done in practice, because that's hardly every where the problems you need help with are. Those are usually found in complex interactions between machines, or your program and the user etc.. So often TLA+ is most useful when the specification is so far above the code level that a direct link is not entirely useful. Having said that, you could use TLA+ to actually prove at the code level by compiling your code to TLA+, as has been done with Isabelle or Coq. This has been done for TLA+ with C and Java, but in practice, code-level verification is not where you'll get the most bang for your buck.

heavenlyblue 8y ago

OK, but could you model Twitter in TLA+ and then would TLA+ be able to find inconsistencies in the model given that you relax certain assumptions? Can TLA+ direct you to which of the caches is being incorrectly invalidated given that you have provided that 10% of the servers online are still using the old version of the software? That seems interesting, but haven't yet played with TLA+ enough to know that.

pron 8y ago
You can't know which of the caches is incorrectly validated, but if you specify the behavior of both new and old versions, you could check to see if mixing them could cause problems. But the more elaborate the specification, the harder it may be to answer the question. Using tools like Coq, you essentially need to write the proof (say, of the claim that mixing the versions could cause no issue with data consistency) yourself. With TLA+ you can do the same, but also have the option of letting the model checker check the theorem automatically for you, but the more elaborate the spec, the longer that would take. This is why you need to learn to specify at a level of detail that's right for answering the questions you want answered -- no lower (higher abstraction), or there may not be sufficient detail to answer them, and no lower, or answering may take a long time. Sometimes you'll find that you're specifying the same system at several levels of detail. One of the cool things in TLA+ is that you can check that the different levels are indeed related (could be a description of the same system at different levels).
- heavenlyblue 8y ago
  On a more practical side of things - how do you mix your application code with TLA+? E.G. Do you have a "proof" project and a the code in different directories with comments in the TLA+ pointing to the files in the actual code? It would be incredibly nice if I could put TLA+ proofs in the comments next to every function or module I am working with and then choosing which of them to be proved. But that seems to be way beyond what the toolset allows you to do.
  - pron 8y ago
    1. Writing formal proofs in TLA+ (or in any other proof assistant) is almost always a waste of time. If the proof is very easy, you can certainly do it, but then you don't need to unless it's a strict requirement or an academic project whose entire purpose is to show that a formal proof is possible rather than some functional correctness requirement. And if the proof is not easy, then there are better methods, like using TLA+'s model checker. 2. Putting references to the TLA+ spec in the code could be nice and useful. 3. You should realize that the benefit from a powerful tool like TLA+ comes when it helps you reason about things that are hard for you to do, and those are hardly ever at the code level. So while using a code-level tool like Why3 to prove some routine is cool, it is hardly ever done in practice, because that's hardly every where the problems you need help with are. Those are usually found in complex interactions between machines, or your program and the user etc.. So often TLA+ is most useful when the specification is so far above the code level that a direct link is not entirely useful. Having said that, you could use TLA+ to actually prove at the code level by compiling your code to TLA+, as has been done with Isabelle or Coq. This has been done for TLA+ with C and Java, but in practice, code-level verification is not where you'll get the most bang for your buck.