3 ms·

Considering you actually have to design around DST, I’m still widely unconvinced that the time and effort spent setting up DST and fuzzing hoping it finds your

Considering you actually have to design around DST, I’m still widely unconvinced that the time and effort spent setting up DST and fuzzing hoping it finds your bugs wouldn’t be better spent actually proving that your design is bug free using tools like TLA+ before intelligently using static analysis and formal proof during implementation. I believe DST to be the wrong solution to the actual problem. Its main advantage is that it doesn’t require that people used to design distributed system actually acquire a new skill set and it doesn’t challenge the status quo too much (after all it’s pretty much just fuzzing on path you have chosen to make fuzzable).

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.

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.