4 ms·
coq allows you to extract a real program, whereas TLA+ just checks a spec for correctness (and you may have bugs implementing it)
by jlrubin 8y ago
coq allows you to extract a real program, whereas TLA+ just checks a spec for correctness (and you may have bugs implementing it)
- pron 8y agoSee my other comment on the matter, but this presents a choice where there is none. No tool that extracts or verifies actual code (and people have actually done both with TLA+) can operate on programs larger than a few thousand lines. So it's not a choice between fully verifying a 200KLOC program or just its 2000-line high-level spec. It's between verifying/extracting a 2000 line program or a 2000 line spec that abstracts a 200KLOC program. In other words, for programs of a certain size, verifying a high-level spec is the only real option for "deep" verification.
- hwayne 8y agoI've seen research tools to extract "real programs" from TLA+. But on the whole not having synthesis as your default case has two major advantages: 1. You can choose the level of modeling, so you can quickly spec out the high level and find bugs in that before moving on to the low level (if you want) 2. It doesn't tie you to an implementation language. So you can use it even if you're implementing in COBOL, JavaScript, or Brainfuck. Of course extraction has its own benefits. Coq is a pretty cool tool :)