stateright VS statig

stateright - which is meant for distributed state machines and includes a full on model checker

Stateright.

Author seems to be using https://github.com/ailidani/paxi for actual implementation and proof.

I'm more of a python/rust guy. There have been some attempts to make model checkers in rust: https://github.com/stateright/stateright

The issue is that rust is a very large language and it's hard to get it right.

I have a python implementation of raft over here:

https://github.com/adsharma/raft/tree/master/raft/states

That's small enough to be self contained and perhaps run through a model checker some day and transpiled to many statically typed languages.

The issue with TLA+ proofs such as:

https://github.com/fpaxos/raft.tla

is that it's hard to tell if a particular C++ or Rust implementation conforms to the spec.

So how do we check and transpile?

* https://www.philipzucker.com/Modelling_TLA_in_z3py/

Why make memory safety the exception? For example, https://github.com/stateright/stateright implements model checking for distributed systems at the library-level. If you could achieve the same effect with memory safety through the ecosystem, why wouldn't you?

Regarding the last point — correct, Stateright aims to verify both.

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...

I believe they meant this: https://github.com/stateright/stateright

I went through multiple iterations for the design before arriving on something that (to me at least) feels clean and is easy to maintain. But of course I’m a bit biased and I’m curious to hear what other people think. So if this sounds interesting to you be sure to check out the repo!

I'm trying to make a blinky app targeting the ESP32-C3 using [statig HSM crate](https://github.com/mdeloof/statig) but I can't figure out how to access pins (or other peripherals) from the states.

The thing is that these handlers can result in different transitions or even no transitions at all (see the calculator example). Maybe one way to think of it is that "state" is the result of all events that have occurred and determines how the system responds to new events. So in that sense the method is the state. (Idk, does that make sense?)