Hi Andrew,
thanks for your response!
On Friday, 10 April 2026 20:24:54 British Summer Time Andrew Helwer wrote:
> Very interesting process! TLA+ is an open source project itself, so it is
> neat to see how involved the contributor vetting process can get.
Yeah, open source projects are wonderful. At Debian, we have a strict vetting
process to keep supply chain attacks and malicious contributions to a bare
minimum. Becoming a core developer is a long process which even involves
meeting at least two vetted developer in person to verify IDs :)
Fortunately, you don't have to be a developer to contribute to Debian. In that
case a Debian Developer reviews the code and uploads it for you.
> I took a
> look at your spec. It is quite nice and I only have minor feedback:
>
> - TLA+ has built-in boolean values, defined as TRUE and FALSE. The set
> of both of them (for type invariant purposes) is BOOLEAN. You can
> probably use booleans for variables like confirmedFreeTime.
Makes sense. Boolean values are more meaningful.
> - The Debian validation process seems somewhat sequential. As you
> probably found, it is slightly annoying keeping track of sequential
> process state in TLA+ (your "applicationState" variable functions as a kind
> of program counter). For this reason, TLA+ has a variant called PlusCal
> which enables you to express this sequential flow in an imperative language
> instead. It transpiles to TLA+, and generates code fairly similar to what
> you wrote. However, using PlusCal is strictly optional here.
+1
I just looked into PlusCal and it is more straightforward than writing plain
TLA+ in that case. From my perspective rewriting the process in PlusCal is
faster than in TLA+.
In the docs there are two flavours (P and C syntax) of PlusCal specified.
Despite the braces, are there meaningful differences?
If there are differences, what is the "recommended" syntax?
> - Your TypeOK is more of a safety property than a type property
> (although the difference is informal). Probably I would make your TypeOK
> invariant look more like some conjuncts of expressions like
> confirmedFreeTime \in BOOLEAN, and then call your current TypeOK
> invariant something like Safety or just Invariant or Inv.
Thanks for pointing this out :)
> - For fun, you could try to think of a temporal property for this
> specification. That would require you to define fairness assumptions on
> your actions, which is kind of amusing because we are asserting fairness
> properties on a person's actions instead of a computer's actuals as per
> usual. A temporal property could be (for example) "every application is
> eventually accepted, under the assumption that the candidate eventually
> makes progress on each individual step".
Good idea. At the moment, I'm rewriting the whole process in PlusCal. After
that I'm gonna take a look and try to implement them. :)
From my perspective TLA+ and PlusCal syntax isn't that hard to learn and the
youtube videos, PDF files etc are great to get started. The hard part is to get
the logic right and think about rules and not about implementations.
> All in all an excellent first spec!
Thanks for your feedback.
Happy Hacking!
--
Arian Ott
arian.ott@xxxxxxxx