I'm intrigued, but having trouble visualizing how even lightweight formal methods can fit into an agile development process at a startup building a web application.
An initial model might take 4 hours to put in place. The time would be spent thinking through how best to abstract the modeled process and its logical properties, slowly building up a more and more complete set of events, and checking the model by running it as one goes. With an initial model, additional hours would probably be spent here and there adding enhancements and finding ways to do things better, just like one would do with regular code. The model would effectively exist over the lifetime of a corresponding code artifact and guide work on the artifact.
For a standard web application that mostly does reads and writes to a database, there usually wouldn't be any need for a tool like TLA to help you reason. A general use case for TLA is describing systems where there are multiple processes or threads coordinating on some sort of shared state.There would be indeterminacy in the order in which events happen. There could be the possibility of failure and the need to handle it gracefully.
- the JS frontend that communicates with AJAX and/or WebSockets IPC with the backend
- the backend may actually be a bunch of microservices
- the fact that there are many concurrent frontends (users)
- messages from frontends may end up reordered/dropped/rerouted on their way to different backend ipc channels (microservices or replicated backend)
- the frontends are untrusted (the user or browser may tamper with your code running there)
- the backend server is also often replicated / sharded
- there are caches (think Redis) that the backends share in addition to the main DB.
- load balancers, high-availability reverse proxies with various failover propreties, etc
- various caching behaviours that are only partly under your control (browser-side content caching, DNS, etc)
- all of the above are interconnected over unreliable channels
- there are secrets and security involved so functional assurance ("pressing button X always makes function Y happen") doesn't tell you enough
(I have no TLA+ experience so can't say how one would use it with a web app, though).
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.
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.
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).
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.
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.