Brief Lang

Brief, an experimental declarative language built around contract-enforced state transitions.

The language models programs as transactions with preconditions and postconditions. Instead of writing control flow directly, you describe valid state transitions, and the compiler is supposed to verify that the transaction satisfies its contract.

It also has, among other variants, an "Embedded Brief" variant, for embedded systems. Which in a lot of cases are state machines, so it seems like a nice fit on the surface.