AI says you’re right, formal methods say you’re wrong

What is TLA+? How does it work?

So TLA+ is a formal specification language.

Okay, we know probably what a specification is, right? We are specifying what are the requirements of our software, what it should do, what it should not do.

But in TLA+ you do that formally, and formally means there is no room for ambiguity, there is no room for interpretation, right? So it's, you're specifying it in a way, and it's that way and, and that's it.

And the way this is achieved, the lack of ambiguity, is by establishing a formal semantics to the syntax, right? So whatever you write there, there is, uh, one precise way about what this means, going all the way back to mathematics and how it's established in mathematics.

So really there's no room for ambiguity.

That's how it was born, to be a precise language to define algorithms, protocols, especially in the distributed systems area.

So TLA+ was created by Leslie Lamport, the father of distributed systems, also creator of Tex for LaTeX.

So Leslie Lamport was writing papers, right? He was coming up with all these distributed systems, algorithms, and he was writing papers, and he realized that he was not being precise.

He found, like, imprecision in his own papers.

And he's like, "Oh, if I'm this, like, super smart person and I'm making these imprecisions, for sure other people are being imprecise as well, and that's a problem.

So let's come up with a shared language we can use." So it was just a language used in papers, and then people realized they could add tooling for that, so you can, like, use machines to check what was written there.

Not only, like, be a precise way of writing it, but actually checking properties.

So they implemented a model checker, the TLC model checker.

It's just an acronym that don't stand for anything.

They don't define what the acronym stands for, just TLC.

That is the model checker for TLA+, which is, you can think of it as like a, the compiler for our language, right? Languages have compilers.

Specification languages, they don't have, like, a compiler that will execute your code or produce executable code.

They have something like a model checker, which is going to verify the code, right? So it takes your TLA+ specifications that will define your specification and check that it is correct.

If I have it correctly, the formal specification is not something you would build a piece of software off of.

You have that first and then have the software f- later.

It would be something to verify that the software you've written meets this specification, right?

There is a big problem with formal methods, which is we don't really have something that, to verify that the actual code is correct.

Like, there are some tools for verifying that the actual code is correct, but they are often very limited because the amount of things you can write in code's very big.

So it's hard to write, for instance, a model checker for Rust.