|
|
|
|
|
|
by tome
3661 days ago
|
|
|
> building a clean model of your program and then proving properties is nice, but without a connection to your implementation the exercise has questionable value This is one thing that has always confused me about TLA+ since pron introduced me to it. Maybe translation of specification into implementation is always the easy part, though ...? |
|
|
Not only is it the easy part, but we're talking about reasoning about programs. If reasoning requires end-to-end certification you're working too hard.
Even within TLA+, you don't work at one refinement level. The lowest level is just too low, and therefore too hard for some proofs. You create a couple of sound refinements -- simpler state machines that capture the relevant essence -- and verify the behavior of yours. It's simpler than it sounds (refinement is just plain old logical implication, =>, in TLA) but it does take effort to reason about -- let alone prove -- a complex algorithm regardless of the formalism you use. FP doesn't make it easier, and it does require more difficult math.