5 ms·
Interesting product. This would be useful for more systems than just graphical user interfaces and frontend development. Backend systems, distributed systems,
by samsquire 3y ago
Interesting product.
This would be useful for more systems than just graphical user interfaces and frontend development.
Backend systems, distributed systems, stateful protocols and microservices are complicated and hard to think about. Raft for example.
I am working on a state machine formulation that is text based and I have an idea which I think would prevent entire classes of bugs.
The idea is that we can see the state machine as a graph and check reachability of states between state machines. If the code literally never fires the event that would cause the reachability of the next state, that's a bug.
The number of times I've been writing some code that uses threads or distributed systems and there is absence of behaviour, it's tricky to debug absence of behaviour.
I've always wanted to "see the future" from my IDE to see what state my code puts everything in.
One of my ideas is the idea of value flow tracing to detect steady state systems, systems that always make forward progress.
- tlarkworthy 3y agoI prototyped this using computational tree logic (CTL). You can express the non existence of trap states and reachability of all states quite nicely and fully explore the state space symbolically. The drawback is you can't really do numbers in it.
- bbkane 3y agoThis is way out of my depth, but you might look into TLA+
- sn9 3y agoHave you read any of Hillel Wayne's stuff? He's got great articles on various formal methods approaches. https://www.hillelwayne.com/tags/formal-methods/ https://www.hillelwayne.com/tags/formal-methods/ Check out the sub-topic tags for more. Or just skim his blog.