4 ms·

The barrier to TLA+ remains the high-cost of rewriting a piece of code in another language. The translation process itself could be error prone. The disintegra

The barrier to TLA+ remains the high-cost of rewriting a piece of code in another language. The translation process itself could be error prone. The disintegrated concepts requires considerable amount of mental effort. I am very interested in using the host language (the language that used to write the software one wants to verify) compiler to compile into a TLA+ spec.

exdsq 6y ago
I believe the main use case of TLA+ is to first design the code as a spec and then implement it, rather than the other way around.
- kinmi 6y ago
  I'd like to learn more: how would one go about ensuring the implementation was an accurate implementation of the specification? Is there a process for doing this?
  - thamer 6y ago
    There's no perfect answer and it's always been a limitation to take into account. There are model-checking solutions which take a spec and generate code, but you don't get this with TLA+. In a way, you could make the same argument about writing tests: the code paths you exercise in your CI environment are not quite the same as what's running in prod, and neither is the environment in which the code is running (e.g. the load your process or host is under, the memory pressure, etc). That said, don't let this small gap and the lack of a perfect solution discourage you from using model checking, there is still a lot to gain from adding it as one more tool in your toolbox.
  - Jtsummers 6y ago
    To the best of my knowledge there's no universal, formal method to translate the spec into code and verify the code properly implements the spec. Just like without TLA+, you're left to conduct your own testing and analysis to verify your code is correct, but with TLA+ you at least have a specification to verify it against (even if it's tedious). That said, some languages offer more capabilities and tooling to support this. Check out Frama-C and its Mthread plugin [0] (NB: I have no experience with either) for something that could help. In Ada there's SPARK, but I'm not sure the extent that it helps with verifying concurrency properties. In some languages, like Erlang, Elixir, and Go, the concurrency mechanism is sufficiently well integrated into the languages that it becomes very clear while reading the code what's happening (especially if you properly segment your code into functions and modules to aid in readability). These can make the analysis much easier to perform. And regardless of language, if you have a specification and design the code tends to come out much cleaner, which makes the manual task of reviewing and verifying these critical parts less onerous. Additionally, it's not as hard to conceive of tests when you have the simpler spec to look at versus the much larger code constructed from it. [0] https://frama-c.com/mthread.html https://frama-c.com/mthread.html
  - aliceryhl 6y ago
    The way I think of it is that TLA+ is a tool for ensuring that the thing you intended to write will work. It's not a tool for checking whether you wrote the thing you intended to.
dwohnitmok 6y ago
This article notwithstanding, I don't think the right mental framework to approach TLA+ is to think of it as a way to verify your code. I view TLA+ as a formal design language. It is there to verify and explore the consequences of architectural and design decisions. It is also there to present a formal design document that engineers can refer to as a common artifact when discussing various design decisions. Now architecture and design is a very vague domain. It could be anything from specific algorithms all the way up to entire distributed systems (and indeed TLA+ can be used for any of those), but the point is that it is a separate entity from code. I also think in the current formal methods environment this is where TLA+ can make the most impact. It is a far less risky business proposition to use TLA+ to record design decisions where the maturity of its toolchain has minimal impact on your actual codebase vs using a formal methods toolchain that directly affects the code you write, where the maturity of that toolchain is an extremely important business decision.
hcarvalhoalves 6y ago
I don't think you can call it "re-writing" when the implementation has to handle a lot of the details that you can and should ignore on the specification. Trying to compile a specification from the implementation would be equivalent to trying to do "top-down" via "bottom-up".
Jtsummers 6y ago
It's not rewriting, it's modeling. And that's a critical distinction. You're able to elide many, if not most, of the details and distill the effort to the critical algorithms and design elements. I don't care how the memory is stored, or even how big, just that it exists (as an example). If I do care, I can add that to the model. And in the case of the example with Go as the implementation language (in the linked article), many of the details (like how channels work) can be reused between specs. This permits analysis of Go programs generally, without needing to respecify Go's concurrency mechanisms every. single. time.
pron 6y ago
I think that the specification in this article -- that tries to do too many things at once -- gives a somewhat wrong impression of how TLA+ is best used. It's not intended to find errors in your code. See my other comment on this matter: https://news.ycombinator.com/item?id=24593196 https://news.ycombinator.com/item?id=24593196 To apply your claim to how TLA+ is best is to say that the problem with architecture is the high cost of having two (or more) representations of the building, once in steel and concrete and once as a blueprint, and conclude it would be better to not have a blueprint at all. The spec is supposed to focus on different things than your code and show the bigger picture. While it would be great to then verify the correctness of your actual program, humanity currently does not possess this capability. The biggest programs ever verified "end-to-end" were ~10KLOC, or 1/5 the size of jQuery, and required years of work by world experts.
- creata 6y ago
  > The biggest programs ever verified "end-to-end" were ~10KLOC, or 1/5 the size of jQuery, and required years of work by world experts. Out of curiosity, what programs are you referring to? seL4 seems to fit the description.
  - pron 6y ago
    seL4 and CompCert are probably the biggest and they both correspond to under 10KLOC of C, i.e. they're very small by modern software standards (and not only are they small and still took years of efforts by experts, they had to be seriously simplified in order for the verification to be feasible). There have been much bigger programs verified with model-checkers (I vaguely recall seeing Samsung mention they model checked a 1MLOC Java program), but in those cases I think the properties were very specific.
- amw-zero 6y ago
  While TLA+ is not intended to verify specific code implementations, we have to admit that that is the holy grail. In my view there are 2 main spheres of practical software: design and construction. Unfortunately, today's construction tools are so error-prone that simply implementing a given design doesn't guarantee that the code is error-free. I think people see TLA+ as an escape from this construction nightmare - because its model is so simple and elegant. I know my wheels have been spinning trying to think about the best way to unify the design and construction processes. So I definitely don't fault people for trying to specify lower and lower levels.
k__ 6y ago
I think it's like writing an outline for an article and writing the actual article. I mean, both tasks are writing, but the outline is on another abstraction level and makes the article a breeze to write.

exdsq 6y ago

I believe the main use case of TLA+ is to first design the code as a spec and then implement it, rather than the other way around.

kinmi 6y ago
I'd like to learn more: how would one go about ensuring the implementation was an accurate implementation of the specification? Is there a process for doing this?
- thamer 6y ago
  There's no perfect answer and it's always been a limitation to take into account. There are model-checking solutions which take a spec and generate code, but you don't get this with TLA+. In a way, you could make the same argument about writing tests: the code paths you exercise in your CI environment are not quite the same as what's running in prod, and neither is the environment in which the code is running (e.g. the load your process or host is under, the memory pressure, etc). That said, don't let this small gap and the lack of a perfect solution discourage you from using model checking, there is still a lot to gain from adding it as one more tool in your toolbox.
- Jtsummers 6y ago
  To the best of my knowledge there's no universal, formal method to translate the spec into code and verify the code properly implements the spec. Just like without TLA+, you're left to conduct your own testing and analysis to verify your code is correct, but with TLA+ you at least have a specification to verify it against (even if it's tedious). That said, some languages offer more capabilities and tooling to support this. Check out Frama-C and its Mthread plugin [0] (NB: I have no experience with either) for something that could help. In Ada there's SPARK, but I'm not sure the extent that it helps with verifying concurrency properties. In some languages, like Erlang, Elixir, and Go, the concurrency mechanism is sufficiently well integrated into the languages that it becomes very clear while reading the code what's happening (especially if you properly segment your code into functions and modules to aid in readability). These can make the analysis much easier to perform. And regardless of language, if you have a specification and design the code tends to come out much cleaner, which makes the manual task of reviewing and verifying these critical parts less onerous. Additionally, it's not as hard to conceive of tests when you have the simpler spec to look at versus the much larger code constructed from it. [0] https://frama-c.com/mthread.html https://frama-c.com/mthread.html
- aliceryhl 6y ago
  The way I think of it is that TLA+ is a tool for ensuring that the thing you intended to write will work. It's not a tool for checking whether you wrote the thing you intended to.

dwohnitmok 6y ago

This article notwithstanding, I don't think the right mental framework to approach TLA+ is to think of it as a way to verify your code. I view TLA+ as a formal design language. It is there to verify and explore the consequences of architectural and design decisions. It is also there to present a formal design document that engineers can refer to as a common artifact when discussing various design decisions. Now architecture and design is a very vague domain. It could be anything from specific algorithms all the way up to entire distributed systems (and indeed TLA+ can be used for any of those), but the point is that it is a separate entity from code. I also think in the current formal methods environment this is where TLA+ can make the most impact. It is a far less risky business proposition to use TLA+ to record design decisions where the maturity of its toolchain has minimal impact on your actual codebase vs using a formal methods toolchain that directly affects the code you write, where the maturity of that toolchain is an extremely important business decision.

hcarvalhoalves 6y ago

I don't think you can call it "re-writing" when the implementation has to handle a lot of the details that you can and should ignore on the specification. Trying to compile a specification from the implementation would be equivalent to trying to do "top-down" via "bottom-up".

Jtsummers 6y ago

It's not rewriting, it's modeling. And that's a critical distinction. You're able to elide many, if not most, of the details and distill the effort to the critical algorithms and design elements. I don't care how the memory is stored, or even how big, just that it exists (as an example). If I do care, I can add that to the model. And in the case of the example with Go as the implementation language (in the linked article), many of the details (like how channels work) can be reused between specs. This permits analysis of Go programs generally, without needing to respecify Go's concurrency mechanisms every. single. time.

pron 6y ago

I think that the specification in this article -- that tries to do too many things at once -- gives a somewhat wrong impression of how TLA+ is best used. It's not intended to find errors in your code. See my other comment on this matter: https://news.ycombinator.com/item?id=24593196 https://news.ycombinator.com/item?id=24593196 To apply your claim to how TLA+ is best is to say that the problem with architecture is the high cost of having two (or more) representations of the building, once in steel and concrete and once as a blueprint, and conclude it would be better to not have a blueprint at all. The spec is supposed to focus on different things than your code and show the bigger picture. While it would be great to then verify the correctness of your actual program, humanity currently does not possess this capability. The biggest programs ever verified "end-to-end" were ~10KLOC, or 1/5 the size of jQuery, and required years of work by world experts.

creata 6y ago
> The biggest programs ever verified "end-to-end" were ~10KLOC, or 1/5 the size of jQuery, and required years of work by world experts. Out of curiosity, what programs are you referring to? seL4 seems to fit the description.
- pron 6y ago
  seL4 and CompCert are probably the biggest and they both correspond to under 10KLOC of C, i.e. they're very small by modern software standards (and not only are they small and still took years of efforts by experts, they had to be seriously simplified in order for the verification to be feasible). There have been much bigger programs verified with model-checkers (I vaguely recall seeing Samsung mention they model checked a 1MLOC Java program), but in those cases I think the properties were very specific.
amw-zero 6y ago
While TLA+ is not intended to verify specific code implementations, we have to admit that that is the holy grail. In my view there are 2 main spheres of practical software: design and construction. Unfortunately, today's construction tools are so error-prone that simply implementing a given design doesn't guarantee that the code is error-free. I think people see TLA+ as an escape from this construction nightmare - because its model is so simple and elegant. I know my wheels have been spinning trying to think about the best way to unify the design and construction processes. So I definitely don't fault people for trying to specify lower and lower levels.

k__ 6y ago

I think it's like writing an outline for an article and writing the actual article. I mean, both tasks are writing, but the outline is on another abstraction level and makes the article a breeze to write.