Agree. But ... I sure hope that the new way of developing distributed systems doesn't follow this pattern:
1. write some code
2. submit to Jepsen
3. if errors, goto 1
The problem with this approach is obvious.
1. write some code
2. submit to Jepsen
3. if errors, goto 1
The problem with this approach is obvious.
The main issue is that distributed database consistency without trivial, performance-killing locking schemes is too complex to prove when writing or using any trivial, local methods based on e.g. SMT solvers or so.
If something like cockroachdb would be proved-consistent on that level, it would be used for applications currently employing pessimistic locking due to a lack of trust in their database, or scaling vertically without really needing to (there are cases which make horizontal scaling cost-prohibitive due to the dependency chains in the algorithms that can solve them, but they can be replaced most of the time).
There's been a lot of work on both of these problems, but right now, proving concurrent algorithms correct, and proving equivalency of those algorithms to executable code, are very much open research problems.