I experimentally implemented Raft in Java but I am not very confident that I did it correctly.
I wish there was a way to implement stateful programs that guarantee "forward progress" and are "steady state systems". I think essentially a state machine that cannot be trapped in a state. Debugging the absence of something of forward moving progress or lack of causation is very difficult.
When there's essentially different actors in the system and they can interact with eachother by communicating, they each have a number of states they can get into. There's no guarantee that the system shall converge on a state that forward progress can be made. Maybe TLA+ is the right answer here.
YMMV but I think (my) reasoning over stateful systems is rather difficult, I think there's lots of hidden states that we cannot easily detect or reason about because they're in our blind spots. Especially related to synchronization. I think it's part of what makes multithreading and distributed systems so hard, because every component can be in a different state and if something is not where it is expected to be, the baton doesn't get passed to the correct state. If you check for something too early, you have a race condition.
If we could see in slow motion what was going on, an interaction between different actors, we could work out why something happens the way it does. But usually the logs are too numerous to get to this detail. I think animation can save us, but what does a Raft animation look like?
How often have you seen an endless spinner? It's as if a completion event was raised but didn't get detected and the system is waiting for something that shall never occur. I want this kind of error to be impossible. This is one form of hidden state that prevents progress.
I wrote an eventually consistent mesh protocol in Python and tested it with Jepsen, it is not linearizable because the consistency level is "eventually consistent".
I don't understand how Raft can scale writes or reads across multiple machines due to the round trip time talking to other nodes.