TLA+ has no direct path to code. But it is a great way to test-drive your _idea_, to force you to dwell on your problem before beginning to code, to look for states that you never thought about even in a simplified setting.

Having gone through the exercise, I find I have greater clarity while coding, and have a better idea of where to place assertions and where to look for invariants. Often I iterate between prototyping with code, then playing with TLA+, then back to prototyping before throwing it all out and starting from scratch.

----

Then there are tools like Coq that convert a proof to running code automatically. For example, see the Verdi framework for doing Raft consensus: https://github.com/uwplse/verdi-raft.

This is clearly not for the faint of heart. The wonderful thing about this exercise is that it forces you to be precise about your specification, and holds your feet to the fire until your proof meets the spec. At the end of the day however, you have no guarantee that the specification (and the simplifications made to get coq going) are enough to capture enough interesting aspects of the real world. Still, for safety-critical and security-critical systems, it is always comforting that someone's gone through the pain of thinking it through to an extra level.

TLA+ could, in principle, be used to directly verify code (e.g. [1]), and has been used like that "in the lab", but then it suffers from the same issues that all code-level, deep specification tools, like Coq, suffer from -- barely being able to get within three orders of magnitude from "ordinary" software.

High-cost end-to-end verification of very small, very specialized programs by experts is a different practice altogether from low-cost, high-level design verification. TLA+ could be used for either, but the biggest bang-for-the-buck, especially in non-super-specialized cases is obviously the latter.

[1]: https://tla2014.loria.fr/slides/methni.pdf

I think that converting C to TLA+ is too low level; TLA's state space would explode before anything of consequence can be explored. There have been similar academic efforts to convert from SPIN's Promela to C, but nothing interesting has been shown.

So, we have TLA+ on the one hand, which is too abstract, and C on the other, which is useless when translated to TLA. I think that a better solution is to have a DSL tailored to the domain, which can generate C for performance as well as a TLA+ model. Anil Madhavapeddy's PhD dissertation is a good example: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-775.html

> TLA's state space would explode before anything of consequence can be explored

You're confusing TLC with TLA+. TLC will work for small programs, but you can still use the TLA+ proof assistant (TLAPS) just as you can use Coq (and for the same definition of "can").

> So, we have TLA+ on the one hand, which is too abstract, and C on the other, which is useless when translated to TLA.

TLA+ is not "too abstract". It is mathematics. It can describe a system at the level of general algorithms, or at the level of logic gates. In fact, it particularly excels at expressing abstraction/refinement relationships between descriptions of the same system at various levels. For example, you can establish a refinement from the C code to a higher-level spec with the proof assistant, and then use TLC to model-check the higher-level spec. But still, TLA+ is not likely to be any better than Coq, or any other deep specification and verification tool. Unfortunately, none of them can feasibly verify software of common size.

> You're confusing TLC with TLA+.

True that. I have not really been able to get anything beyond the most trivial to work with TLC, so I just stick to TLA+.

> TLA+ is not "too abstract". It is mathematics.

I understand. I'd wager that is the chief reason why most programmers don't even begin to investigate it. Spin feels easier because it is operational and because it can incorporate C.

> I have not really been able to get anything beyond the most trivial to work with TLC, so I just stick to TLA+.

Really? I personally have checked quite elaborate TLA+ specifications with TLC, and I know others have, too. Sure, like all verification tools it's got its limits, but even for a complex distributed system spec, TLC could reasonably check it with, say, four nodes.

> I'd wager that is the chief reason why most programmers don't even begin to investigate it.

I'm not sure Spin is used more than TLA+ these days, especially when it comes to "mainstream" software.

Thank you for this explanation, without which I would have continued searching for a mirage. Everything makes a lot more sense now. It would be great if TLA+ made this clear (or at least clearer) right from the start.

I've actually built something like this for TLA+ and C#, which I call Kayfabe. I'll hopefully present it this October at the next TLA+ conference.

High-level, there are two modes:

1. Checking execution traces from running code against the model (see notpron's work for this idea)

2. Outputting every state visited by the model checker in a finite instantiation, then computing paths to step the real C# through so it'll visit every state or transition at least once. This is very, extremely computationally expensive, but I'm running real code in prod that I've tested this way.

Hopefully I can get my algorithms to be efficient and if so I'll try to open-source my efforts.

I'm really interested in these ideas any chance you can share your progress before October?

I'm excited to see this!

You are asking the wrong question. While there are various ways to check conformance to the spec, none of them guarantees it. In fact, no one knows how to do that using any tool whatsoever. People sometimes refer to end-to-end verification successes (verifying all the way from the spec to the code or even machine code) like seL4, but forget how tiny that codebase is, how long it took specialized experts to write and verify it, and what concessions had to be made to make that possible.

So let me ask you this: how do you guarantee that your tests cover all possible case? You can't (and they probably don't). So why do you use tests at all? Because the question isn't how to guarantee the software is perfect -- something we can't do, at least not currently -- but how to make it better. And just like tests can make your software better even if it's not perfect, a TLA+ specification can, too.

How do you go from a blueprint to the program? The same way you go from an algorithm in a book to a program. You can make the specification as detailed or as high-level as you like, and focus on whatever you think is the most important parts. Going from spec to code is the easy part.

TLA+ was created so you can quickly model / specify a design, check it works under your assumed invariants and maybe explore alternatives up front, giving you a plan for how your system should work in theory.

Like you mentioned it's the software blueprint, and you go from a blueprint to a building by actually building the thing - TLA+ is not made to codegen your product.

Would you say that it's closer to "pseudocode you can use to test process assumptions" than a description of the final structure that a program would have?

Yes apart from it's not pseudocode but mathematical formulas.

Your building blueprints aren't made from bricks and mortar because it would just take way longer and be expensive to experiment with, however with software when designing we often use the same tools as building without thinking of the cost like that.

TLA+ and other lightweight modelling languages allow you to experiment with your design and verify that it works without all the tedium of programming languages and their environments / libraries / compilers etc.

huh, I guess I’m going to have to try it because I just realized that I had a hidden assumption that code was definitionally the lightest way to describe a problem

A lot of people use PlusCal, which is basically pseudocode that compiles to TLA+. Depending on what you're modeling, PlusCal or directly writing TLA+ might be a better fit.

I think that's fair. It's been described elsewhere as 'exhaustively testable pseudocode'.

Look at idris - proofs are expressed using dependent types which allow full propositional logic and implementations exploit these proofs using a haskell like language that allows imperative + purely functional code: https://www.idris-lang.org/

There are more: F* compiles to Ocaml/F#/C/ASM/WASM [1] and it's variant Low*, and ATS [2], which compiles to C.

  [1] https://www.fstar-lang.org/
  [2] http://www.ats-lang.org/

Dependent type theory doesn't directly model the concepts of TLA+ (e.g., an eventually modality), so this doesn't really answer the question.

Different proof tools inhabit different areas on the "specification to implementation" spectrum (problem/solution). Since it's possibly to perfectly implement a bad specification, proving a specification valid has value, even if it isn't formally proving your implementation of that spec.

Typically, before implementing a feature it'd be nice to have a design for it. Nothing that takes 6 months, though. TLA+ would be really helpful there, especially if you become familiar with it, so that you can answer the "what if" questions.

I think I will give it a try. It might definitely help building better distributed systems.

Code review. Lots and lots of code review!