I think this has been the case for many decades. Lamport, the Turing award winning mathematician and computer scientist who wrote seminal algorithms and papers on distributed consensus, invented TLA+ for this express purpose.

A programming language is insufficiently expressive enough to specify and guarantee the safety and liveness properties of a multi-agent system.

I think formal methods and program synthesis are going to become the tools of choice in the long term for designing reliable systems in this vein.

I've been following the development of the CALM theorem and various attempts at programming languages that implement it's ideas (BloomL, etc) since 2010 at least -- I'd wished I knew about TLA+ back then. This paper is great... I hope it catches on more.

What's a good small project + stack for someone to start with formal methods and/or program synthesis?

For an introduction and motivation to TLA+ I recommend Hillel Wayne's talk Everything About Distributed Systems is Terrible [0] and basically anything he has written on his blog about the TLA+.

I think following along with the TLA+ video course is really thorough and digestible once you've decided that you want to learn more [1].

You'll find the TLA+ Hyperbook is a useful reference and guide as you start specifying your own systems [2]. It has a number of examples and projects to work on.

Eventually if you want to go deep after you've decided it's worth it for yourself, get into Specifying Systems the text book and bible of TLA+ [3].

Program Synthesis has a lot of research in it and is starting to show promising results. I'd say that while the research has been going on for a long time it's still rather new to industrial use... for a motivating talk and explanation on what program synthesis is try this one: https://www.youtube.com/watch?v=HnOix9TFy1A

[0] https://www.hillelwayne.com/talks/distributed-systems-tlaplu...

[1] https://lamport.azurewebsites.net/video/videos.html

[2] https://lamport.azurewebsites.net/tla/hyperbook.html

[3] https://lamport.azurewebsites.net/tla/book.html

Thanks!

I'd actually suggest rather becoming fluent in modern Haskell.

Formal methods are great in their own way but for a lot of programming tasks they overshoot the mark. For those that do not, by all means, bring them in. But right now, a practical engineer can't ignore just how klunky they are and how badly they scale up. One may gaze longingly at them, and dream fondly of the future date when they are more practical, but they aren't there yet.

There is a reason the Haskell community is always banging on about monads and monoids and applicative functors and commutivity and associativity and identifying exactly how little power you need to accomplish a given task, and it's the same reason I was able to say in another comment thread that Haskell is probably the only current semi-popular language that could deploy the ideas in this paper as a library, and that library would actually be correct. (There are some languages that could deploy the library and it would be a cultural fit, like OCaml or Clojure, but you'd still be able to trivially use it incorrectly.)

Plus even if you still want to get into formal methods and program synthesis, "learn Haskell first" is still a fairly sensible stepping stone. It probably isn't strictly mathematically true, but formal methods are going to be more-or-less a superset of what modern Haskell teaches you anyhow. Both the Haskell language and the Haskell tooling will be easier, and pragmatic enough you can do a real project like "rewrite my website in it" or other pragmatic, attainable projects that the formal methods languages can't do yet.

Many formal methods have a much simpler mathematical foundation than Haskell. For example, for TLA+ the background includes mostly (basic) set theory, basic logic, and some additional bits of temporal logic.

Some methods do require a lot more math, or different math, but I'd say your statement is false for the majority of popular formal methods.

Indeed, I heard Lamport say at a talk (in response to a question) that he saw little or no applications of functional programming to the distributed systems problems he was interested in.

Formal verification is really hard because you have to use mathematical proof to show that a piece of software does what it should on all inputs and paths. You have to formalize the software, the desired goals, and prove a connection. Typically, you have to do this for software written in languages that aren't designed for verification. That makes it even harder.

This led me to recommend people start with so-called lightweight, formal methods that require less upfront learning with more automation. You'll see the value of formal methods, have more fun, and maybe use it on realistic problems. The best one to start with is Design-by-Contract invented by Meyer in the 1980's based on principles from 1960's. Contracts are simply precise, declarative descriptions of a module expects from callers, does during execution, and returns to the caller. Here's an overview even a project manager can find useful:

https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...

A number of us independently arrived at a specific use for contracts that's high ROI. You use contracts to specify intent, then automatically generate tests from them (replaces unit testing), and finally they can become runtime checks for automated testing (esp fuzzing). Contract-based tests or fuzzing with contract-based checks cause each failure to take you right to the source of the problem. Note that the test generation part has many names to Google: specification- or spec-based, model-based, and recently property-based testing. Hillel Wayne has great posts on contracts and test generation:

https://hillelwayne.com/post/contracts/

https://hillelwayne.com/post/pbt-contracts/

I recommend reading his whole blog. Anyway, the next tool is Alloy which is super-simple but with better tooling than most academic works. Hillel has examples on his blog. Davidk01 on Lobste.rs has been using it for a lot of things. He said, given its relational, he just uses it like he uses SQL:

https://lobste.rs/s/ghhcus/test_generation_from_bounded_alge...

Finally, one that will help you with protocols and concurrency is TLA+. Hillel has learntla.com up to teach you for free on top of blog examples. After a lot more time with it, he got to publish a book through Apress. I recommend it:

https://www.betterworldbooks.com/product/detail/Practical-TL...

If you want a taste of proof, the SPARK Ada language was designed to make it easier. It's used in industry. Basically uses contract-like specs and supporting functions to feed "verification conditions" into automated solvers. You only have to prove what they can't but can always use runtime checks on those. There's a nice book teaching you how to use it plus Altran/Praxis' Correct-by-Construction method for low-defect software.

https://www.betterworldbooks.com/product/detail/Building-Hig...

There's also Cleanroom: a 1980's method that combines semi-formal specs, simple use of language, hierarchical composition, and usage-based testing to cost-effectively get high quality software. Stavely has best intro to it:

http://infohost.nmt.edu/~al/cseet-paper.html

https://www.betterworldbooks.com/product/detail/Toward-Zero-...

Note: Linking to Better World Books since they're a public-benefit type of company (see History). Amazon ain't. ;)

Nice list!

For proofs I've been finding the leap into dependent-type theory to be very productive as many provers in this realm also double as practical programming languages allowing the possibility of shipping proof-carrying code.

My two favorites in this area are Lean [0] and Agda [1], the latter of which recently received a nice introductory text from Phil Wadler and Wen Kokke [2].

[0] https://leanprover.github.io/ [1] https://wiki.portal.chalmers.se/agda/pmwiki.php [2] https://plfa.github.io/

When people say that "programming doesn't involve mathematics", I think they really mean that programming doesn't involve hard mathematics. It's obvious that computers can only calculate, and meta-calculation is mathematics. However, most people have this notion that math is hard, and many programming tasks are easy.

Then, you take a look at a distributed system. Every task is substantially harder in a distributed system. The answers are not obvious, so folks are more willing to accept that those things are math.

I disagree, I think the future still holds separate data layer, but even less math because of how much easier it will be to reason about programs with DSLs built on solid foundations for distributed systems and how much harder it will be to keep doing things the old ways. Imagine a new language for databases, like SQL, but that can actually guarantee convergence and coordination freedom, where there are no transactions and weird behaviors with weird consistency violations and slow complex buggy implementations, but where everything just works and all you have to do is just be a bit more creative in mapping real world problems into that model. Not that the model can't be too expressive, it might even be able to express directly a lot of traditional non-monotonic stuff.

I think you'll find that if you encode these guarantees into the language level itself, that won't allow the programmers involved to stop thinking about the math. Either your language won't allow them to express the first thing they want to express, and they'll have to figure out how to do it with the proper mathematical primitives (and they'll complain up a storm about how useless your language is on the forums), or it will allow them to express it but yield a compile-time "Operation violates monotonicity constraints at line 88..." and they're going to have to understand that fairly deeply, or also end up dropping your language when they can't scale up their program because the "blunder around adding and removing sigils and annotations and sprinkling in 'unsafe' until the compiler shuts up" just doesn't scale very far beyond "complete the school assignment due tomorrow".

Look at Rust. Putting memory management concerns in the language front and center doesn't relieve you from having to thinking about them. It means you have to think even more deeply about them. Fortunately, this is the correct thing to do, and it get easier with practice, and is also easier to learn when it's so strongly highlighted instead of implied and buried. But if anything, it forces a more mathematical way of thinking on to you. (Reasoning about scopes is the foundation of the mathematical discipline of structured programming.)

I mostly agree, but I think any new mathematical understanding will be an implicit one. For example, in Rust, although the underlying type system is affine, almost no one explicitly reasons about programs using affine logic

It’s funny; I think of Rust as freeing me from having to think of this. The compiler checks it for me, so I just don’t have to think about it at all.

We aren’t there yet, but we are approaching the day when substantially everyone with the capability of rebalancing a red/black tree on a whiteboard and an inclination to program is either programming or in some other way connected to the function. If a yet higher level of mathematical ability and knowledge becomes necessary, shortages are going to become even more acute. That’s good for some of us but bad for the world. The world would be better off if we could figure out a way to lower that bar, not raise it.

I'm being honest here I don't quite understand all the math involved . But from my rough skimming of the text looks like we are sacrificing the flexibility to change any input or minor design changes for guaranteed correctness .. am I wrong

It's more like "the flexibility to change any input" produces incorrect behavior, full stop.

When it comes to distributed systems, you have to be following some mathematical idea of how you're going to maintain some sort of consistency or correctness, or it just won't happen. The environment is just so much more hostile than the ones most people are used to. Most programming methodologies haven't grown up in the presence of an adversary that, for all practical purposes, is out to get you.

Another such discipline is the security domain, and we're having the same sorts of issues there, too. As a whole community, we're really just beginning to grapple with the idea of programming in an environment that has hostile, intelligent entities out to get you. There's still a contingent of people who insist it's not even an issue! Though it's shrinking fairly rapidly.

I respect what you are trying to say and im not denying that safety as a mathatical guarantee is a must .. but help me understand the full picture here how would such a system work with soft dev today when requirements change very quickly, sometimes small somtimes large ... for example our current sdlc looks like this

mockup --> requirement change --> design --> build --> requirement change --> mockup

rinse and repeat, the cycle time might change but this is what happens .. is this ideal I don't know .. does this work, it does sufficiently enough

and so I disagree that people in the broader software dev community are willfully ignorant about security

maybe with the rise of AI we could do the design problem with the math bits in mind and build correct software every cycle but from my perspective the only way I see the system of mathematical design which is math intensive (hence resource intensive hence time intensive) is through the waterfall model of SDLC :).

I am willing to admit that I haven't been following the formal methods space that much and what I said might be complete of the mark, in any case, please feel free to correct me, I'm here to learn thanks.