> 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

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