Hacker News Reader

Comment by oconnore | Hacker News Reader

Huh? The whole point of distributed algorithms is that a set of local algorithms create a global behavior. I received this message so I send that message, etc. The SPARK contracts you write would check that local behavior, and the TLA+ would check that that local behavior results in some global behavior.

View on HN

Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.

You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, and the local contract ensures that the local behavior of the various actors is correct -- and therefore results in that emergent behavior. Combined, that's a fairly solid argument that your system does what you intended.

If you had to implement the full proof in Ada, there would be no point to doing the TLA+ work.

"You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, "

This is how I was seeing it happen, too.

Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes sense.

Its just a little out of scope of the current thread, because the author of parent message was talking about using pure Ada/SPARK, without help of TLA+ (As I understand it in the first place), so my comment about using contracts was in that context.

No, I meant implementation in SPARK. The specs were already done in TLA+ in the OP's model. There's also implied porting between two notations.

Reply on news.ycombinator.com