These thing are so exciting, but as a regular web dev I always wonder what are some real use cases?
Most stuff can be done without any of the fancy containerization and such solutions.
Most stuff can be done without any of the fancy containerization and such solutions.
Whatever things you end up deciding, does your system, where many people are reserving, cancelling, and re-reserving over long periods of time, guarantee all of the client's expectations?
How would you prove to the client that your solution implements these requirements? Modeling the system using a language like TLA+ is one way of doing that.
There is no reason to start implementing things, if your design is wrong.
Formal Specification proves your design, while Formal Verification proves your implementation.
As far as I understand this project - Stateright does both (i.e. 2-in-1). Kind of executable model?
It’s important to clarify that this doesn’t provide a proof of correctness, but it can dramatically improve confidence in both the design and implementation compared with fuzz testing, for example. This is done by exhaustively enumerating possible nondeterministic outcomes (e.g. due to message reordering) within specified constraints (e.g. up to S servers and C clients performing X operations…).
Examples:
SD Paxos: https://github.com/stateright/stateright/blob/master/example...
ABD (linearizable register algorithm): https://github.com/stateright/stateright/blob/master/example...
If you don't have that (say you're using TLA+), one really promising technique is to generate behavioral traces and then refine those into code tests. I know a few companies have done this successfully, and I've been working on some examples of how it's done, but to my knowledge there's no battle-tested tooling that do this automatically. It's all bespoke for now.
Having a specification which is guaranteed to be correct before implementation begins is a programmer’s wet dream.
One of my dreams is to flatten that learning curve. I don't think we'll ever make these tools effortless, but I think it's possible to reach a point where "these tools are too hard to learn" isn't a barrier anymore.
(Even then, I imagine a lot of people will learn some formal specification, and think "this isn't useful for me", and never touch them again. And that's fine. But I want anybody to be able to reach the point where they can make that decision, as opposed to feeling like they're locked out by default. We have a long way to go, but I think we're considerably further along than we were five years ago.)
> Having a specification which is guaranteed to be correct before implementation begins is a programmer’s wet dream.
I wouldn't say guaranteed to be correct, but at least it's, like, closer to correct? Less likely to have horrific bugs, or bizarre edge cases in the requirements that nobody notices until neck deep into the implementation. Stuff that increases founded confidence.
That said, implementing a consensus algorithm is quite hard. Modeling and testing is much harder, there is even a language just for this purpose; TLA+ [0].