Re: [tlaplus] TLA+ project meetings - Minutes January 10, 2023

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

Meeting Minutes January 10, 2023

Participants
• Mamoun Filali
• Martin Hornacek
• Igor Konnov
• Markus Kuppe
• Leslie Lamport
• Calvin Loncaric
• Stephan Merz
• Sam Miller
• Zac Policzer

Introduction

In the context of setting up the TLA+ Foundation, which should be completed shortly, the objective of this meeting is to gather developers and users of TLA+ and of its support tools in order to discuss interests, issues, and possible contributions. The scope of the meeting does not include funding issues, which are the domain of the future foundation. Participants introduce themselves and their interest in TLA+. 

Current work on TLA+

Markus teaches TLA+ and advises users on how to write specifications. He works on performance improvements for TLC, including scaling up expression evaluation and better parallelization. He also looks at using reinforcement learning for guiding random simulation. Stephan has been working on TLAPS, including extending it for proving liveness properties. He is interested in monitoring distributed programs with the help of TLA+ specifications. Igor has been developing the Apalache tool, which includes a bounded model checker based on SMT encodings and techniques for random symbolic evaluation of specifications. He works on extending the scope of specifications handled by Apalache (including checking liveness properties) and on optimizing the tool. Based on feedback from the crypto community, he is investigating an alternative syntax that would be more acceptable to users. Calvin is interested in the usability and functionality of the tools and documents problems in the form of GitHub issues.

Possible areas of future work

What are the barriers to TLA+ adoption and use? How can we make it easier for contributors to find issues to work on?

• Mamoun would like to see more automation in generating proof obligations, similar to what exists for Event-B. The "decompose proof" dialog is of help, but the Toolbox interface is not easy to extend.
• Markus adds that TLAPS should be supported by the VSCode extension. Similarly, Apalache lacks any GUI support. Implementing this would require a developer who is sufficiently knowledgeable about using the tool. Purely browser-based use of Apalache probably requires more thinking.
• What's the future of GUIs for the TLA+ tools? The community of Eclipse developers is shrinking. An advantage of VSCode is that it can be used from any browser using GitHub code spaces. A browser-based IDE without requiring a GitHub account (and beyond the restrictions imposed by the free tier) would be even more attractive. TLC's cloud mode was an attempt in this direction but it fell apart due to incompatibilities between the APIs of different cloud vendors.
• The protocol relating TLC and the Toolbox is based on parsing TLC's text output and is described in a 2019 paper at F-IDE (https://arxiv.org/abs/1912.10633v1). It has significant limitations, and Markus suggests switching to an RMI-based architecture for future Java-based GUI integration.
• The builds of the Toolbox and of the TLA tools should be separated so that tool developers do not need to set up a Toolbox development environment.
• Documentation for developers is lacking / outdated, which makes it difficult for new developers to contribute. Sam Miller offers to add better documentation.  An corresponding issues has been created at https://github.com/tlaplus/tlaplus/issues/778.
• GitHub issues are not sufficiently categorized for letting people discover good first issues. The "Help wanted" label goes some way but is too unspecific. Markus created a “good first issue” label: https://github.com/tlaplus/tlaplus/labels/good%20first%20issue


You can find the full recording of yesterday’s project meeting at https://youtu.be/mbZ8CKckq5A


Per our calendar [1], the next project meeting is scheduled for February 14th at 8 am Pacific Time.

Markus

[1] https://calendar.google.com/calendar/u/0/embed?src=cb3f93f188c92378a8fec42b25365ab2a64665d770a8265c1fcec00e03823c6c@xxxxxxxxxxxxxxxxxxxxxxxxx&ctz=America/Los_Angeles

> On Nov 22, 2022, at 9:56 AM, Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:
> 
> Hi all,
> 
> to foster broad collaborations, we will start hosting monthly meetings to coordinate and discuss ongoing and future TLA+ development.  Please join the meetings if you want to become involved or actively contribute to the TLA+ project [1].  The inaugural meeting is on January 10th at 8 am Pacific Time [2].
> 
> Markus
> 
> [1] https://github.com/tlaplus
> [2] https://calendar.google.com/calendar/embed?src=cb3f93f188c92378a8fec42b25365ab2a64665d770a8265c1fcec00e03823c6c%40group.calendar.google.com&ctz=America%2FLos_Angeles

-- 
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/605DCECD-23F5-45DE-90F6-6B5BFA3DFDC6%40lemmster.de.