Proving that your algorithmic design is correct (to the degree the proof tool can assure) is already a big help - even if your implementation of the algorithm might still have bugs.

At least now you know it's just bugs you need to fix, and not a faulty logic to begin with.

Faulty logic can only be proven to a specific mathematical limit, if the actual system constraints, hardware and OS APIs, aren't part of the model.

My comment was already about proofs "to a specific mathematical limit" still being useful and better than nothing, tho

TLA+ helps to find errors in your algorithm. It's a way easier than trying to model the algorithm in terms of end implementation. Too much complexity and state are introduced because of details.

Abstract algorithms in mathematical sense, not algorithms that depend on hardware and OS constraints.

It can model that if you add it. You can model total or partial hardware failure if you want and its a case you care about, you can add steps that corrupt your data or steps that kills machines at any time. TLA+ is just a way of defining state transitions and temporal properties, inside that add the use cases you need and it will handle them just fine.

And then calling that C API, that Vulkan shader with a broken SPIR-V driver, the automated router firmware update done overnight, just brings down all the hard verification work, done in an external tool.

So because a tool doesn't fix everything it's best not to use it? Each tool has its place, its uses and their limitations. You buy a car even if it doesn't cook you food. If you have multiprocess algorithms, distributed systems or concurrency at all, TLA+ is a lifesaver to understand and fix fundamental issues in your system, if you care about a broken shader, it's just not your tool. When there is a bug you can discard a whole part of the problems and you can check the implementation against a known specification that works.

I wouldn't think I need to explain this to a professional developer, if you are waiting for the silver bullet that solves all your problems you may as well go take care of goats.

To pick up your example, it is more like getting the driver license with only the theorical written test, and only thereafter drive a car for the very first time on the road with the newly received license.

Yes, we should be open minded, and the tools should also be improved so that developers on the trenches bother to learn and use them.

You are clearly engaging in bad faith at this point when you pick the "car not being useful for everything" analogy and you cherrypick it into absurdity. For someone that says is interested in distributed algorithms it's clear you are not interested in being able to reason, about them.

EDIT: There was an edit adding the final part of the comment after I submitted mine above. Here is my response to the last part, since the comment was toned down a bit:

Yes, we need to improve the tooling, and TLA+ can be improved a lot, I'd love for it to be able to reason about my code and to have an easier bridge between both words. However engaging in the discussion of how it can be improved without acknowledging what good and usefulness it brings is just not useful in general, and it just puts off people that could benefit from it from ever using it.

TLA+ has a lot of value in some cases, and we should be acknowledging that!

Yes. And they could contain errors even without OS and hardware. And practice clearly shows it. Proofs are easier to make on the same abstraction level, aren't they?

For that you would need a proper, well-grounded type system and a language that doesn’t stray from it.

Some fp languages are close enough to fit that bill; Rust too is going down this path: its type system was built to make a proof, after all.

I don't know if that's always the case. My understanding is that TLA+ is really designed to prove properties about algorithms. Knowing that complex algorithms are correct is very useful eventually if it doesn't provide a correct implementation in a real world language.

But TLA+ is a bit of an unusual proof language. I think most of them are like you describe: SPARK, Dafny, F*, CBMC, all the Rust ones, etc. I'm not sure about the interactive proof languages (Coq et al), they are too complicated for my normal sized brain.

Yes, and making those languages (SPARK, Dafny, F*, CBMC,....) more widespread, the kind of something that everyone expects to be out of the box on their favourite language is how this can eventually gain more adoption, than a few selected companies, or academic research.

The main issue is that proofs take almost literally forever to write. You cut your productivity by a factor of 100-1000 if you want to prove things.

Not my experience (with Alloy and TLA+, some FM are very very hard and time intensive), it takes me a day to have a decently sized proof of some pretty complex difficult to test algorithms. The idea is not to use it for everything. But testing, thinking about and ensuring the validity of my solution with TLA+ is a lot faster than without TLA+. Not only that, but if any time in the future you need to add something to the system you can add that in half an hour and make sure all your important invariants hold without having to put yourself again in "paranoid mode" and having to remember everything about the system. Tests help, but some things are very very hard to test properly.

As everything it is a tradeoff, a lot of things do not deserve a proof, but for the ones that do you are a lot more productive.

It also depends on the level of the proof, I want to make sure the idea is valid and it takes some time to know what to abstract and what not to (it is a model after all). So if you are aware of what you are testing and at ehat level the tool and your proof is working it is very beneficial

The visible "productivity" as in manager friendly LOC. The actual productivity goes up.

Managers don't want that though, for reasons that already Dijkstra has outlined.

I'm a researcher in formal verification; my thesis was building a tool to do this kind of stuff and I agree with the grandparent (though I would say probably closer to 5-10x slowdown not 100x).

Proofs are hard and often not for interesting reasons; its stuff like proving that you won't overflow a 2^64 counter which you only increment (aka something which won't happen for another couple billion years).

Current tools are only useful for specific kinds of problems in specific domains; things where a life really depends on correctness. Outside of those cases, lightweight techniques provide much more bang for your buck imo.

My formal proofs for C or C++ take almost no time to write at all, because I'm using the right tools. Some asserts, some _CPROVE_assume hints, and mostly limitation of big for loops or recursions. If it works for 6, it also should work for 1000.

I do not know TLA+, but there is an abundance of other theorem provers that can model C very closely, including overflow, assignments, etc.

So closely, that when you transcribe such an algorithm to C, there is very little room for error, even if the C code isn't proven directly.

> there is an abundance of other theorem provers that can model C very closely

Can you list some/all of them please? Would be helpful to others here.

> doesn't mean when the algorithm gets actually implemented in C, it still maps to TLA+ as proven.

So true, but you know what would be amazing and useful? A TLA+ spec transpiler that emits fuzzing code. That would probably be easier to make than TLA+ spec transpiler that emits C.

There are tools available for direct formal analysis of the system as implemented (and not “just” a model of it).

With e.g. the C bounded model checker CBMC, your model language is also C. Frama-C is another approach (Hoare-like, axiomatic logic). Klee works on LLVM IR etc.

Stronger proponents would perhaps suggest extracting the implementation from the model etc., but you don’t have to drink all the koolaid at once to get many of the benefits.

And not all your software needs to be formalized either, to get many of the benefits.

I’ved succesfully used CBMC and Klee on C code for verifying important parts of embedded safety/mission critical software on resource constrained HW (i.e. no OS, static allocation, single to double digit kilobytes of RAM etc.)

Formal methods rock!

Can you recommend some good resources on these over and above their main websites ?

"most of these tools like TLA+, live in another dimension, proving something in TLA+, doesn't mean..."

This sentiment is sloppy, dismissive, with an tinge of obligation to bend to old man wisdom. I don't buy it for a moment.

Let's do better.

Formal tools help suss out requirements solved with high level algos for selected hard sub-issues of the problem under consideration. It's not code to be sure. And, this argument cuts both ways.

It's also far from a clear a pile of code knows, expresses, implements, or communicates its requirements. Just because the code compiles doesn't necessarily mean squat either.

So first thing: specification and implementation are both important and walk hand in hand. How tightly you hold onto one or both depends on several factors such as: are you competent in formal tools (learning them is tough), are there really hard sub-problems e.g. distributed computing on the table? etc.

Second, I want to deal with risk ... you know ... connecting the dots end-to-end in software from customer to requirements to coded. I'll motivate my point with a imaginary story.

In Silicon Valley two companies A, B on opposite corners of the same block are having a big team meeting. The big boss is in with important news.

Company A: We just got a huge, new sale 10x our normal size. They want our basic product but with a lot of extensions, customizations. Business will get you situated with it. Effective now we're suspending our current work. All team leads and lead techs are required to meet with business to assess work planning, risk, task order, deliverables, and so on. We expect this work to run for 18 months. In that time we may abandon, re-prioritize, and clarify work as coordinate with the customer. The customer may change their mind etc.. But as we know well, coding the product goes hand in hand with risk, discovering clearer requirements, and doing a better job of delivering them. We're equal to it.

Company B: We just got a huge, new sale 10x our normal size. They want our basic product but with a lot of extensions, customizations. Business will get you situated with it. Effective now we're suspending our current work. Part of this new work requires us to glue feedback from three controllers, plus sensors in realtime to compute steering commands to the cockpit console. If we nail this, there's 100x more work for us. Given how crucial this aspect is, we'll use Lean, Spin to model requirements and work out some LTL to make sure we're on the right path before we code. We expect this work to run for 18 months minimum. In that time we may abandon, re-prioritize, and ....

Now at this point the boss at company B is cut off with a bunch of whining from its developers:

* formal live in another dimension

* a good model doesn't mean right requirements

* even if the model is right there's no proof it's implemented right

* it'll take longer to do because we've added scope

* etc..

The boss at company A, B are both doing the right thing. Both companies have risk - a lot of it. But company A has engineers on staff who are preternaturally good at dealing with risk. Company B, unfortunately doesn't really understand risk at all in terms of doing something about it.

In this story company A never talked about formal tools. That's on purpose. I want to emphasize only that the problem to be impacted is risk levels, risk location, and sensible ways to manage it. Here formal is but a tool. It's not magic. It's just a tool. Had the boss at A mentioned formal tools, engineers would have rolled with it seeing it as one more bullet in their armory.