Re: [tlaplus] Re: Using TLA+ for data modeling

TLA+ has already been used extensively at Intel and Amazon and many other industrial projects that qualify as being a "real system". TLA+ does not solve our problem, it does not force us to think in any special way, therefore it is extremely flexible. We may specify digital systems in any formal language that best suits our requirements, it is entirely up to our decision.

TLA+ is based on an elegant observation that computations can be specified using a couple of mathematical formulas. Some people find TLA+ to be the natural way of thinking about concurrent or distributed systems. We can use naming and hierarchical decomposition to specify even the most complex systems such as the real-time operating system designed by Eric Verhulst and his team.

Formal Specifications have been used to generate code for so many years, and it works, however it does not necessarily generate efficient code. We do not write TLA+ specs to generate code from them, we use them to understand the system that we are trying to build. Our design lives at a higher level compared to actual code. We are interested in the correctness of our systems, not catching implementation errors. The reason behind this approach is the unnecessary complexity of programming languages that ties our hand and may mislead us as well.

AmirHossein

On Mon, Nov 25, 2019 at 10:46 AM <clifford.heath@xxxxxxxxx> wrote:

Chris,

Looking back at this I wish it had not taken me so long to understand it. Having now played with TLA+, I think everything you've said is spot-on.

However I think that for designing and implementing real systems, a more humanised approach than TLA+ is needed to defining operations. I've written to you privately about the "decision/action" extensions to CQL, which I think others here might wish to enquire about. I won't dump my thoughts into this old thread, but just mention that I'm still thinking about this problem. Rather than merely verifying the code, the specification could be generated to a guaranteed-correct implementation. With the operations defined in the syntax of the model, any error scenarios that TLA+ finds could also be verbalised. In other words, it could explain in English why your code is wrong and how it will fail.

Also, the CQL specification has been rewritten and is published at <http://cjheath.github.com/activefacts-cql> in case anyone is wanting that.

Further, on verbalisation, I have now received a copy of the PhD thesis by Shin Huey where she developed ORMv2 verbalisations for Mandarin and Malay. It was a more difficult problem even than Terry Halpin expected, but it is done!

Clifford Heath.

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/f944a6db-7453-4417-bd6c-44651d05e549%40googlegroups.com.