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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.

Hi,

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.

Cheers,
Markus

[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.