> as very confusing for me to understand how you can trust the implementation unless you can compile TLA+ to C.
Preach. I feel like I'm taking crazy pills every time someone claims TLA+ as the sine qua non of provably correct systems. They should sub probably for provably.
There is no contradiction here, TLA+ is mostly about proving properties of toy models, not end-to-end proofs about real programs. As TLA+ practitioners like to point out, the latter is only applicable to favorable "local" properties - this is what type systems do, they state claims that are quite aligned with the program's syntactic structure; or else to rather trivial programs where proving "whole-program" claims is still feasible. Even Verus itself doesn't really change this.
Isn’t the value in being able to verify the design before implementing? It would be more ideal surely to prove correctness of the deployed code, but I still find it very useful.
Preach. I feel like I'm taking crazy pills every time someone claims TLA+ as the sine qua non of provably correct systems. They should sub probably for provably.