[tlaplus] Re: Temporal collisions in at-least-once message brokers — formal verification with TLA+ templates

[Neil Talap <khairtalap@xxxxxxxxx>]

The broker is too often used in horribly designed systems. I don't think
 it's an overstatement to simply call almost all, if not all, systems 
that use bus decoupling incorrectly designed. People lean on them too 
hard for the decoupling they think to be scalable. Yet they never design
 for the correct invariants. It irritates me, to say the least, when 
reading about it.

To verify events in a bus, you cannot only 
verify the events themselves; you now have to verify every single 
service, or at least faithfully model every component, that connects to 
the bus if those components affect the invariant you're trying to prove.

And
 as a result, you don't get a verified implementation; you can never 
state the implementation has been verified. It has only been modeled. 
Lamport designed TLA+ for this exact purpose, for people to first think 
about the system and invariants before writing any code.

This assumption is too strong: "the protocol is the same, only the variable names change"; this itself is not an invariant.

If your goal is to verify systems, TLA+ has never been designed to do that; it was designed to force engineers to think first.
To ask: What is the system? What are its states? What must always remain true?

Only after answering those questions should code exist.

On that note, I must say I believe buses have a place and time for 
their use. But I also believe virtually all implementations are 
incorrect and were utilized as a result of a dogma. I also believe these
 very same people never use them correctly. The bar for good engineering
 has fallen even lower in recent years.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/885d2336-4477-4b6d-a45d-8d8b94418d2cn%40googlegroups.com.