Hacker News Reader

Comment by symplee | Hacker News Reader

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.

View on HN

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

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

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.

Hence using humans.

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.

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.

The problem is that the training required for "proof monkeys" is higher than for programmers, so they'll be even more expensive (plus you need to know the specified C semantics to prove C code, something even many/most C programmers don't know), and second, the proving effort is not something that can usually be done separately and after-the-fact. The program needs to be written in a way informed by the proving effort. Moreover, every time the program is changed, the amount of proof that needs to be rewritten could be large, especially if the programmers are unfamiliar with the proofs.

Hopefully, there are more efficient formal methods than the one that is currently the least efficient of them all.

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

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?

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

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

[2]: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

Most software is boring and derivative.

Doesn't really matter if only unrealistic edge cases are unprovable.

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.

So the ones that aren't edge cases can still benefit greatly, rather than not at all.

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.

Reply on news.ycombinator.com