Formal methods: Just good engineering practice?

The main issue is that most of these tools like TLA+, live in another dimension, proving something in TLA+, doesn't mean when the algorithm gets actually implemented in C, it still maps to TLA+ as proven.

Formal methods need to be like SPARK 2014, or DbC, actually part of the programming language, or being able to generate code in the target language, interop with its libraries ecosystem, and have good quality good with performance, that won't make people want to remove the generated code and rewrite it manually.

I like the quote:

  “It would be well if engineering were less generally thought of, and even defined, as the art of constructing. In a certain important sense it is rather the art of not constructing; or, to define it rudely but not inaptly, it is the art of doing that well with one dollar, which any bungler can do with two after a fashion.” Arthur Wellington

Where is the boundary between finance and engineering? And Engineering is also about making optimal tradeoffs in other dimensions (he mentions time, performance, scalability, sustainability, and efficiency).

In my opinion formal methods are what's missing from software engineering to make it a serious engineering discipline. In all other engineering fields you have to produce calculations and "proofs" that your design ought to work. In software engineering everything is basically overcomplicated handwaving.

In my opinion, most developers should be using bounded model checking if available for their language / platform. This is certainly true for C, Rust, Java, and others.

I consider bounded model checking to be "formal methods lite". It provides most of the benefits at a lower cost of entry than using a proof assistant or building constructive proofs. Really, there's little added overhead. Perhaps 30% to 40% more time to build out the function contracts and model checking. Given that this overhead more or less prevents errors that would likely be introduced without it, I think it's a reasonable investment.

TLA+ is certainly related, since it uses an SMT solver at its base. I see it as useful for designing algorithms and protocols. A tool like CBMC or Kani provides similar guarantees at the source code level. It's not perfect, as currently CProver does not have direct threading support, but with a reasonable application of method shadowing and function contracts, even things like threading can be anticipated. Using a bounded model checker effectively means changing the design of software to work best with it. This is little different than using concepts like TDD or continuous integration.

Non-software engineering doesn't excessively use formal methods. Only where required. (Like where a system is tightly optimized.)

For instance, in electronic engineering, you don't use the most accurate model of a diode at all times. Sometimes it's just a one-way valve. Sometimes, it's just one-way valve with a 0.7V drop (if silicon).

In mass production, you will not get the accurate parts needed for the most formal model to be justifiable, and the cost of those parts would not be justified in most of the circuitry.

Is there formal methods 'tooling' similar to TLA+ that is more targeted to State Machine design and perhaps State Machine Replication?

I learned some TLA+ and started reading about Coq, but I was pretty disappointed to learn of the "verification gap" between the the algorithm to be delivered in a normal programming language and the manually-restated algorithm that passed the checker. We need to make a checker's input language ergonomic enough for daily use and then "synthesize" something that runs efficiently while still being known correct, or make a checker understand everyday programs (which, not being so minimalist, probably have a much larger space of reachable states to check).

I worked for a [Japanese] corporation, that took “formal methods” into overdrive.

They made really, really good hardware, but it was extremely painful for us software schlubs.

That said, I don’t know if it’s really possible to do really big stuff, with a team, unless you have some degree of formality.

Best practices are usually a good place to start, and I would suggest that the degree of necessary formality, is inversely proportional to the experience of the team. If you have a lot of really experienced engineers, in a mature team that has been together a long time, the formality is still there, but doesn’t need to be written down.

I usually work alone, or as the sole technical person, in a diverse team. I’m really experienced, and don’t write much down.

But I’m also really, really formal. It just doesn’t look like it.

I think we might potentially be looking at this backwards. There is a great talk by Jack Rusher [1] on why having really slow iteration loops and being too disconnected from running programs creates a desire for theorem proving because it becomes the faster way to arrive at a correct solution.

I am of the belief that we need to return to modifying live environments instead of sending code through a lengthy build pipeline. Instead of trying to make live environments secure and durable we got scared and now we have modern CI/CD.

[1] https://www.youtube.com/watch?v=8Ab3ArE8W3s

I do often employ the simple whiteboard methods described, but I've never found the energy to learn and use stuff like TLA+. What fields do people find them useful in?

> What is TLA+? > > TLA+ is a formal language for specifying systems used in industry and academia to verify complex distributed and concurrent systems. Among others, the TLA+ methodology is successfully applied at Amazon Web Services, Microsoft, and Oracle.

https://conf.tlapl.us/home/

Just wanted to post this video link in this discussion:

Glenn Vanderburg - Real Software Engineering

https://www.youtube.com/watch?v=RhdlBHHimeM

"Beware of bugs in the above code; I have only proved it correct, not tried it. " -- Donald Knuth