[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] How do you do functions of structures?

On 07.06.21 09:24, Aaron Elligsen wrote:
However true, I did find it unfortunate. The primary purpose of the record is to group associated data together. You can point out the isomorphism all day but that doesn't change the fact that it is easier to reason about related data when it is in the same place. Neither object oriented or functional programming languages really encourage destructuring data in this way. It goes against the grain of most programmers training for modularity and encapsulation. It also likely makes the TLA+ specification diverge from the code that it is trying to describe so verifying equivalent states between a production system and the tla spec will now need another translation step to either destructure or restructure the data for comparison.


specifications are not code. Concepts that organize programs that span dozens or hundreds of files are usually overhead for specs that consist of a handful of files. I certainly don't organize my bookshelf the same way librarians do to keep thousands of books in order.

Many concepts in TLA+ go against the (my) training of programmers, which is best summarized by: "we witnessed first hand the brain washing done by years of [...] programming" [1]. The concepts indeed appear strange to us, but strangeness doesn't invalidate them. If all the strange concepts were replaced in favor of familiar ones, TLA+ would be another programming language.

The conundrum that makes it challenging to keep specs and code in sync are the abstractions that we want to find with TLA+.

Perhaps PlusCal could provide a key word to handle the conversion automatically. I can see either nested records or set unions creating complications, but maybe this would be good enough for most situations.

There are other proposals to extend or fork PlusCal. If there is a group of people who write PlusCal specs that are too large, the parties could team up and propose and implement an extension of PlusCal with additional modularity concepts (I believe the term "modular pluscal" is already taken). The recently created RFC [1] repository would be a good place to organize and discuss the work.


[1] https://lamport.azurewebsites.net/tla/industrial-use.html?unhideBut=hide-rtos&unhideDiv=rtos&back-link=high-level-view.html
[2] https://github.com/tlaplus/rfcs

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/f142af41-fff5-9cf3-a1c0-75d7eb54d612%40lemmster.de.