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.
Using math to model a system instead of learning math qua math does wonders for ease of understanding. Derivates and integrals become easy if you're using them to model the relationship between position/velocity/acceleration. I don't think I really got linear algebra until using it to learn quantum computing.
You mind seems to be trapped in the employment binary where you're either a full-time W-2 employee or you're unemployed. With contracting and startups it isn't so simple. Contractors (especially ones working in boutique niches on scoped projects) might work for a month with much time between contracts. During that down time maybe they write blog posts or contribute to OSS or hang out with someone else prototyping some neat ideas that don't pan out (which might reasonably be called a startup after the fact) or just do literally nothing so as to recover from burnout, which is lethal to the contractor in a way it isn't to an employee. All of which feed into more people dropping into their inbox inquiring about their contracting availability. It isn't "lying" to say time spent not working on a paid contract is time spent in service of contracting.
Beyond the distasteful idea that we should always act in a way demonstrating obedience to potential employers, the solution to this is extremely easy. Gap year? No! I am merely doing independent consulting. Do I actually have any contracts? So many questions!
Plus if you actually use the time to work on OSS instead of traveling or whatever I have no idea how an employer (that you'd want to work at) could fault you for that. Seems like a huge asset.
Software seems to be doing okay, jobs-wise. The number of recruiters showing up in my inbox hasn't changed. I think health insurance is included in the severance.
Hope Cosmos team releases a whitepaper on their experiences with the language. I'd heard snatches of gossip here and there that TLA+ was used inside Cosmos, but no concrete details.