3 ms·

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 n

by 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.

by pron 6y ago

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.