[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" . 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
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  repository would be a good
place to organize and discuss the work.
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.