6 ms·

The next big breakthrough will be a program that can convert TLA+ directly into production code. And create all of the necessary tests, with a formal proof that

The next big breakthrough will be a program that can convert TLA+ directly into production code. And create all of the necessary tests, with a formal proof that the code is correct.

AnimalMuppet 7y ago
Your program may be able to formally prove that the code corresponds to the TLA+. It may be able to generate tests to show that the code does what the TLA+ says it should do. But a program can't prove that the TLA+ is correct[1]. The most it could prove is that it is not self-inconsistent. So now you move from debugging the production code to debugging the TLA+. That's still an improvement. [1] Unless you take the TLA+ code to be the definition of "correct". That's a possible position, but I don't adhere to it. It seems to me more reasonable to be able to say that the spec is wrong if it doesn't correspond to what is actually needed, and the TLA+ is wrong if it doesn't accurately encode the spec. (For example, the MCAS software did exactly what the spec said. But the spec was wrong.)
- galaxyLogic 7y ago
  But how do you unambiguously specify "what is needed"? I would think you need some high-level formal language for doing that. So I wonder if instead of proving that some hand-written code corresponds to a specification, wouldn't it be better to think of the specification as a high-level program and then somehow translate into some lower level conventional programming language?
  - TuringTest 7y ago
    > But how do you unambiguously specify "what is needed"? You don't. You follow the scientific method of building a model specification for "what is needed", throwing it into the world, and tweaking and improving it where you find that some of its properties are not a good fit for the problem it's intended to solve - primarily by gathering feedback from the people that are using it and finding its flaws.
ampdepolymerase 7y ago
It already exists (not with TLA+ but for other formal systems). This is bog standard code synthesis. Problem is that it does not scale very well. There is a better way: https://news.ycombinator.com/item?id=22278363 https://news.ycombinator.com/item?id=22278363
- pron 7y ago
  Our (sound) formal verification tools and knowledge are nowhere near anything that could do this affordably for programs of common sizes, and it's unclear they ever will be (the gap between programs we can verify soundly and the size of the programs we write has state roughly constant for decades). The hottest approach these days in formal methods that operate directly on code of real-world-sized programs is reducing the soundness of verification with approaches like concolic testing.
  - ampdepolymerase 7y ago
    Hence using humans.
    - pron 7y ago
      Humans don't do this affordably. Programs proven end-to-end correct using human provers and semi-automated proof assistants have required extreme simplification of the program so that it could be verified at all (so no clever efficient algorithms), teams of graduate-student proof-monkeys working for years, and even then the biggest programs we could prove that way were ~10KLOC. The greatest achievement of this semi-automated approach required years by highly-trained specialists to prove simplified programs that amount to 1/5th of jQuery. We have some very interesting advances in formal verification, but that is probably not the way.
      - ampdepolymerase 7y ago
        If you see my comment, it proposes using large infosys style teams. You don't need graduates per se, just people who have an intuition for logic and math, of which there are plenty. Plus you can prove isolated pieces e.g. TCP/IP stacks instead of end-to-end. It would not be as beneficial as full formal verification but it is still a large step in securing the most vulnerable targets such as IoT, industrial control systems, financial services etc.
maxfan8 7y ago
This is not always possible due to the halting problem [1] and Gödel's incompleteness theorems [2]. It is not always possible to formally determine/prove the behavior of a program. [1]: https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem [2]: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
- lallysingh 7y ago
  Most software is boring and derivative.
- Groxx 7y ago
  Doesn't really matter if only unrealistic edge cases are unprovable.
  - TuringTest 7y ago
    The problem is, you don't know that. The software industry is this complex because obscure yet realistic edge cases happen much more often than you'd expect.
    - Groxx 7y ago
      So the ones that aren't edge cases can still benefit greatly, rather than not at all.
      - TuringTest 7y ago
        What good is applying formal verification software to have proof that part of your input behaves properly, but edge cases are not proven? This is already what test cases do.
dwohnitmok 7y ago
I actually think the opposite is true. TLA+'s strength in a business context is precisely because it is not production code. This considerably derisks TLA+ because you cannot end up depending on TLA+, or put another way any deficiencies in TLA+ or its toolchain will not become production blockers for your team. You cannot lose more time than the time you spent writing your spec. You can use TLA+ to specify as much or as little of your system as you want. You can upgrade your system independently of TLA+. You don't have to wait for TLA+ to support or integrate with your language. I've said this elsewhere, but the closest competitor to TLA+ on most teams is decent high-level documentation, which is precisely what most teams lack. Software tools, like many other things, suffer from an uncanny valley effect. If you're not tempted at all depend on a tool to generate code for you, you know the limits of the tool and can be quite happy. If the tool integrates smoothly with the rest of your code it's even better. However, if your tool integrates in a somewhat bumpy way with the rest of your code than it becomes worse than the two previous alternatives. The TLA+ community already has limited resources that I think can be better spent on making TLA+ an even better design language before trying to cross the much bigger and more arduous gap of trying to make TLA+ executable (a goal which I suspect most of the community would actually oppose anyways).

The next big breakthrough will be a program that can convert TLA+ directly into production code. And create all of the necessary tests, with a formal proof that the code is correct.

AnimalMuppet 7y ago

Your program may be able to formally prove that the code corresponds to the TLA+. It may be able to generate tests to show that the code does what the TLA+ says it should do. But a program can't prove that the TLA+ is correct[1]. The most it could prove is that it is not self-inconsistent. So now you move from debugging the production code to debugging the TLA+. That's still an improvement. [1] Unless you take the TLA+ code to be the definition of "correct". That's a possible position, but I don't adhere to it. It seems to me more reasonable to be able to say that the spec is wrong if it doesn't correspond to what is actually needed, and the TLA+ is wrong if it doesn't accurately encode the spec. (For example, the MCAS software did exactly what the spec said. But the spec was wrong.)

galaxyLogic 7y ago
But how do you unambiguously specify "what is needed"? I would think you need some high-level formal language for doing that. So I wonder if instead of proving that some hand-written code corresponds to a specification, wouldn't it be better to think of the specification as a high-level program and then somehow translate into some lower level conventional programming language?
- TuringTest 7y ago
  > But how do you unambiguously specify "what is needed"? You don't. You follow the scientific method of building a model specification for "what is needed", throwing it into the world, and tweaking and improving it where you find that some of its properties are not a good fit for the problem it's intended to solve - primarily by gathering feedback from the people that are using it and finding its flaws.

ampdepolymerase 7y ago

It already exists (not with TLA+ but for other formal systems). This is bog standard code synthesis. Problem is that it does not scale very well. There is a better way: https://news.ycombinator.com/item?id=22278363 https://news.ycombinator.com/item?id=22278363

pron 7y ago
Our (sound) formal verification tools and knowledge are nowhere near anything that could do this affordably for programs of common sizes, and it's unclear they ever will be (the gap between programs we can verify soundly and the size of the programs we write has state roughly constant for decades). The hottest approach these days in formal methods that operate directly on code of real-world-sized programs is reducing the soundness of verification with approaches like concolic testing.
- ampdepolymerase 7y ago
  Hence using humans.
  - pron 7y ago
    Humans don't do this affordably. Programs proven end-to-end correct using human provers and semi-automated proof assistants have required extreme simplification of the program so that it could be verified at all (so no clever efficient algorithms), teams of graduate-student proof-monkeys working for years, and even then the biggest programs we could prove that way were ~10KLOC. The greatest achievement of this semi-automated approach required years by highly-trained specialists to prove simplified programs that amount to 1/5th of jQuery. We have some very interesting advances in formal verification, but that is probably not the way.
    - ampdepolymerase 7y ago
      If you see my comment, it proposes using large infosys style teams. You don't need graduates per se, just people who have an intuition for logic and math, of which there are plenty. Plus you can prove isolated pieces e.g. TCP/IP stacks instead of end-to-end. It would not be as beneficial as full formal verification but it is still a large step in securing the most vulnerable targets such as IoT, industrial control systems, financial services etc.

maxfan8 7y ago

This is not always possible due to the halting problem [1] and Gödel's incompleteness theorems [2]. It is not always possible to formally determine/prove the behavior of a program. [1]: https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem [2]: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

lallysingh 7y ago
Most software is boring and derivative.
Groxx 7y ago
Doesn't really matter if only unrealistic edge cases are unprovable.
- TuringTest 7y ago
  The problem is, you don't know that. The software industry is this complex because obscure yet realistic edge cases happen much more often than you'd expect.
  - Groxx 7y ago
    So the ones that aren't edge cases can still benefit greatly, rather than not at all.
    - TuringTest 7y ago
      What good is applying formal verification software to have proof that part of your input behaves properly, but edge cases are not proven? This is already what test cases do.

dwohnitmok 7y ago

I actually think the opposite is true. TLA+'s strength in a business context is precisely because it is not production code. This considerably derisks TLA+ because you cannot end up depending on TLA+, or put another way any deficiencies in TLA+ or its toolchain will not become production blockers for your team. You cannot lose more time than the time you spent writing your spec. You can use TLA+ to specify as much or as little of your system as you want. You can upgrade your system independently of TLA+. You don't have to wait for TLA+ to support or integrate with your language. I've said this elsewhere, but the closest competitor to TLA+ on most teams is decent high-level documentation, which is precisely what most teams lack. Software tools, like many other things, suffer from an uncanny valley effect. If you're not tempted at all depend on a tool to generate code for you, you know the limits of the tool and can be quite happy. If the tool integrates smoothly with the rest of your code it's even better. However, if your tool integrates in a somewhat bumpy way with the rest of your code than it becomes worse than the two previous alternatives. The TLA+ community already has limited resources that I think can be better spent on making TLA+ an even better design language before trying to cross the much bigger and more arduous gap of trying to make TLA+ executable (a goal which I suspect most of the community would actually oppose anyways).