2 ms·
> 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 ever
by jgalt212 16d ago
> 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.
- zozbot234 16d agoThere 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.
- digilypse 16d agoIsn’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.
- jgalt212 15d ago> Isn’t the value in being able to verify the design before implementing? Fair enough, but to be truly safe you really need the whole pipeline connected. model -> validation -> emitted code.