Yeah, the tooling potential is huge for TLA+. The gap between what it could be, and what it is, tooling wise, is enormous.
I’d be more ambitious though: it seems worthwhile to do just a full-stack re-implementation? A written-in-go-or-rust tla+ binary which is a model checker a formatter an lsp server a debugger a documentation generator for TLA would be a major improvement over the current stack.
Now, I only dabbled with TLA a bit, so maybe my tooling perspective is wrong here, but, with the small amount of data I have, I have a strong feeling that full-stack re-implementation is the way to go.
All of the people with the resources and expertise to do a full-stack reimplementation are making their own specification languages instead. TLA+ is too powerful: it’s hard to parse, hard to write, and only a subset of it can be feasibly model-checked.
are making their own specification languages instead.
Are there some which are production ready enough to specify something like Paxos? I finding myself needing to specify a thing, and shopping for TLA+ alternatives
I do want to RIIR, but figure I would need at least a years’ worth of money saved up for the work. If someone wants to pay me like $60-70kish I would do it! Until then I’ll just do contracts to save up the money.
I’m especially interested in adding type checking to the language. I assume it would be very difficult but very fun. Definitely not feasible in the general case, but it could get good integration with the built-in proof language to help it along.
It actually does sound like people might throw money at it, but, speaking from rust-analyzer experience, that usually comes after something is already working. Which is indeed a dilemma!
Yeah, there is an effort underway to set up a TLA⁺ project under the Linux Foundation (see https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ) but I suspect maintaining/expanding the current tools will monopolize whatever money comes in there. Rewrites of this sort will have to come from self-funded outsiders until they gain enough traction to justify spending foundation money on them, similar to what has happened with the TLA⁺ VS Code extension. Is that what happened with rust-analyzer?
I can’t speak for the early days of rust-analyzer, but I did a bit of the monetary side - funding it from the Ferrous Systems side and setting up and running the OpenCollective. I’m happy to share insights and experience if you are interested. I’m currently a bit unavailable, but if you send me an email to florian.gilcher@ferrous-systems.com, I’ll get back to you.
I’d like more people to self-fund themselves in Open Source - it isn’t magic, but also not quite as simple, so experience-sharing is what I can offer.
Yeah, I’ve spent half a year burning through my money, then Ferrous Systems chipped in, and maybe after a year more the project was established enough for various things like open collective to become meaningful.
Types in TLA+ is a very interesting topic. First, how would that even work? TLA+ is untyped at its core, and I’m not sure how types would affect the soundness of the logic?
Interestingly, there is an embedding of TLA (note the lack of +) in Isabelle/HOL, which is a typed logic:
Mostly I’m hoping to catch very simple things, like going variable.fieldname where that variable isn’t set to a record with that field name. Clearly this collapses to automated theorem proving in the general case since variables can take on absolutely arbitrary values from one state to the next but most model-checkable specs are written in an idiomatic way where each variable has a pretty simple type invariant like variable \in set. It would certainly be a best-effort sort of thing.
Thanks for sharing your experience, very enjoyable read.
Tangentially, I considered a similar project and it was what finally made me leave Emacs. I wanted syntax highlighting for Alloy in Emacs and I thought for sure that I’d make a lot of progress in an afternoon, but I learned about font lock mode and syntax tables, and the whole thing just felt like an annoying mess. I definitely looked into tree-sitter, and it seemed like a way better approach than the standard Emacs way.
I gave up in an afternoon. Great to hear your experience sticking out for the long haul.
Yeah, the tooling potential is huge for TLA+. The gap between what it could be, and what it is, tooling wise, is enormous.
I’d be more ambitious though: it seems worthwhile to do just a full-stack re-implementation? A written-in-go-or-rust
tla+binary which is a model checker a formatter an lsp server a debugger a documentation generator for TLA would be a major improvement over the current stack.Now, I only dabbled with TLA a bit, so maybe my tooling perspective is wrong here, but, with the small amount of data I have, I have a strong feeling that full-stack re-implementation is the way to go.
All of the people with the resources and expertise to do a full-stack reimplementation are making their own specification languages instead. TLA+ is too powerful: it’s hard to parse, hard to write, and only a subset of it can be feasibly model-checked.
Are there some which are production ready enough to specify something like Paxos? I finding myself needing to specify a thing, and shopping for TLA+ alternatives
I do want to RIIR, but figure I would need at least a years’ worth of money saved up for the work. If someone wants to pay me like $60-70kish I would do it! Until then I’ll just do contracts to save up the money.
I’m especially interested in adding type checking to the language. I assume it would be very difficult but very fun. Definitely not feasible in the general case, but it could get good integration with the built-in proof language to help it along.
It actually does sound like people might throw money at it, but, speaking from rust-analyzer experience, that usually comes after something is already working. Which is indeed a dilemma!
Yeah, there is an effort underway to set up a TLA⁺ project under the Linux Foundation (see https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ) but I suspect maintaining/expanding the current tools will monopolize whatever money comes in there. Rewrites of this sort will have to come from self-funded outsiders until they gain enough traction to justify spending foundation money on them, similar to what has happened with the TLA⁺ VS Code extension. Is that what happened with rust-analyzer?
I can’t speak for the early days of rust-analyzer, but I did a bit of the monetary side - funding it from the Ferrous Systems side and setting up and running the OpenCollective. I’m happy to share insights and experience if you are interested. I’m currently a bit unavailable, but if you send me an email to florian.gilcher@ferrous-systems.com, I’ll get back to you.
I’d like more people to self-fund themselves in Open Source - it isn’t magic, but also not quite as simple, so experience-sharing is what I can offer.
Yeah, I’ve spent half a year burning through my money, then Ferrous Systems chipped in, and maybe after a year more the project was established enough for various things like open collective to become meaningful.
Types in TLA+ is a very interesting topic. First, how would that even work? TLA+ is untyped at its core, and I’m not sure how types would affect the soundness of the logic?
Interestingly, there is an embedding of TLA (note the lack of +) in Isabelle/HOL, which is a typed logic:
I honestly have no idea what the implications of that are, but maybe there’s some useful info there.
Mostly I’m hoping to catch very simple things, like going
variable.fieldnamewhere that variable isn’t set to a record with that field name. Clearly this collapses to automated theorem proving in the general case since variables can take on absolutely arbitrary values from one state to the next but most model-checkable specs are written in an idiomatic way where each variable has a pretty simple type invariant likevariable \in set. It would certainly be a best-effort sort of thing.Thanks for sharing your experience, very enjoyable read.
Tangentially, I considered a similar project and it was what finally made me leave Emacs. I wanted syntax highlighting for Alloy in Emacs and I thought for sure that I’d make a lot of progress in an afternoon, but I learned about font lock mode and syntax tables, and the whole thing just felt like an annoying mess. I definitely looked into tree-sitter, and it seemed like a way better approach than the standard Emacs way.
I gave up in an afternoon. Great to hear your experience sticking out for the long haul.
I guess some Emacs developers agree — https://lobste.rs/s/h0apsh/emacs_29_is_nigh_what_can_we_expect.
The latest emacs release had tree-sitter integration as a banner feature, so you might not be estranged for long!