There is a strong Jevons Paradox effect at play here though, people generally have a set amount of wall-clock time (1 minute, 10 minutes, etc.) they budget to check their model and then find the largest model that fits within that wall-clock time. So really this just increases the size of the state space people will explore, which might be the difference between checking, say, 3 vs. 5 nodes in a distributed system.
That's very neat! I will look at Truffle. The TLA+ interpreter is definitely "weird" in that it does this double duty of both evaluating a predicate while also using that same predicate to extract hints about possible next states. I wonder how well this highly unusual side-effectful pattern can be captured in Truffle.
Edit: okay the more I look into GraalVM the more impressed I am. I will have to sit down and really go through their docs. Oracle was actually cooking here.
There are some proposals floating around to evolve PlusCal. Probably the most prominent is Distributed PlusCal[0]. There's a programming language lab at UBC which is also doing a lot of experimentation with transpiling PlusCal to Golang[1]. They presented a paper at the latest community event.
The PlusCal-to-TLA+ transpiler is considered part of the core TLA+ tools and will definitely keep being maintained.
There has definitely been a focus on improving developer onboarding in the past few years! If someone's PR is rejected now that can be considered a failure of the process, something to be fixed. I think when TLA+ was mostly a product of MSR this sort of thing could kind of fly (still unfortunate) but now that we're out in the wild with a foundation it's really a survival thing to not bounce willing contributors.
Hillel Wayne wrote a post[0] about this issue recently, but on a practical level I think I want to address it by writing a "how-to" on trace validation & model-based testing. There are a lot of projects out there that have tried this, where you either get your formal model to generate events that push your system around the state space or you collect traces from your system and validate that they're a correct behavior of your specification. Unfortunately, there isn't a good guide out there on how to do this; everybody kind of rolls their own, presents the conference talk, rinse repeat.
But yeah, that's basically the answer to the conformance problem for these sort of lightweight formal methods. Trace validation or model-based testing.
To be totally fair, my article is about the problem of writing specs when your product features could change week to week, whereas I think u/alfalfasprout is talking about regular updates to an existing system slowly bringing it out of sync with the spec. For the latter problem, yeah trace validation and model-based testing is the best approach we have so far.
why are the lower case L's in that document bolded? a different weight? Not sure what the right technical change term is for the visual difference but it was extremely noticeable immediately upon opening the document
I think it is good that people put in a lot of effort to collect this in one place. The report opens with a very strong perspective:
>The case against Stallman is clear, and yet the free software community has failed to act, in particular at the level of institutions and leadership but also in the form of grassroots support for Stallman. Many defenses of Stallman rely on a comfortable ignorance: ignorance of the scope and depth of Stallman’s political campaign against women and victims of sexual violence, or a comfortable belief that Stallman ceased his problematic behavior following his 2021 re-instatement in the Free Software Foundation. Some believe that Stallman’s speech has not caused material harm, or that his fringe views are not taken seriously; we provide evidence to dismiss all of these arguments in this report.
One thing I have consistently encountered when discussing contentious topics with people is that intentional ignorance is a tactic. One cannot be held responsible for acting one way or another on an issue if they do not know anything about it. Women I know in industry report this as by far the most common reaction of male coworkers to one of their colleagues facing allegations of sexual harassment. They don't know anything about it, it seems complicated, they haven't followed it closely, they don't want to get involved, etc. It is very frustrating and I am glad the report has identified this phenomenon and is pointing out this has been going on for long enough that it cannot be reasonably deployed by anybody.
I worked through this a few years ago and it is wonderful, but I found chapter 9 on the replace function totally impenetrable, so I wrote a blog post in the same dialogue style intended as a gentler prelude to it. A few people have emailed me saying they found it and it helped them. https://ahelwer.ca/post/2022-10-13-little-typer-ch9/
This is great for me for a completely auxiliary reason, which is that I wanted to know whether this was just gonna be a book about programming Fibonacci numbers into types or some ish... and in some ways it's kinda worse, at chapter 9 you are still proving that different takes on x→x+1 are the same. (But using rewrite rules seems kinda interesting in the abstract I guess.)
This series of books has always been aimed at people who want to implement the underlying systems. If you’re more interested in the application side of dependent types you might like the book Functional Programming in Lean by the same author, which is freely available online!
Good way to describe it. I tend to see it occur on lists alongside The Art of War and The Prince, which have this weird reputation as titanic, dense tomes read by Serious Men but in reality are more like pamphlets that you can go through in about half an hour. The first time I saw a copy of The Art of War in person I actually laughed out loud.
reply