4 ms·
One of the big problems with using TLA+ is that it verifies your design, not your code. People are looking for ways to link the two. Formal proof works but is t
by hwayne 2y ago
One of the big problems with using TLA+ is that it verifies your design, not your code. People are looking for ways to link the two. Formal proof works but is too expensive for most businesses.
The most promising approach I've seen so far is... DST! First we simulate a system, we generate a bunch of timelines, then we see if those timelines are valid behaviors in the TLA+ design. I've heard of a few success stories and it's definitely cheaper than formal proof!
- RandomThoughts3 2y ago> The most promising approach I've seen so far is... DST! First we simulate a system, we generate a bunch of timelines, then we see if those timelines are valid behaviors in the TLA+ design. That’s just testing again. That’s not linking the code to the design. DST feels to me like the way people treated memory access before Rust came around. Doing things properly was also seen as too costly then but now that it’s trendy everyone is fully behind lifetime tracking. Same here, formal proof is “too costly” but spray and pray approach like DST is somehow acceptable. Anyway, keeping with the Rust example I guess I just have to wait two decades and the next generation might finally see the light.