[4ad]

Comparison with TLA+ doesn't make any sense as TLA+ implements a very different sort of logic, but the property that it is a real programming language is shared by virtually everything in this space.

Lean/Adga are real programming languages, while Coq (Rocq), F*, ATS, Isabelle/HOL all extract to various other programming languages.

Frankly, it's TLA+ that is the odd one here.

[pjmlp]

Agreed, my remark was more coming from the point of view that I don't get why TLA+ keeps being talked about, when there is such an impedance mismatch between the math model proving the logic, and the actual implementation, where even the language semantics might play a role that wasn't clearly mapped on TLA+ model.

[steego]

Isn't TLA+ is more like Alloy insofar as they're thinking tools optimized for the design phase?

I'm more familiar with Alloy, which is a great tool for exploring a specification and looking for counter-examples that violate your specification.

AFAIK, none of the languages you listed above work well in conceptualization phase. Are any of them capable of synthesizing counter-examples out of the box? (Aside: I feel like Lean's meta capabilities could be leveraged to do this.)

[pjmlp]

I only listed Dafny, although I do agree with the list on the reply to me.

Never looked into Alloy, I guess have to get an understanding of it.

How can you validate that the beautiful design phase actually maps to e.g. C code, writing data via ODBC to a SQL database, with stored procedures written in PL/SQL?

Neither the semantics of the toolchains nor the semantics of the commercial products ar part of the TLA+ model as such.

Additionally it requires someone to meticulously compare the mathematical model with the implementation code, to validate that what is written actually maps to what was designed.

Although it wouldn't work for my contrieved example, at least tools like Dafny have more viability by going through "formal model => generate library for consumption", so that we can get an automated model to code validation, without human intervention.

[Jtsummers]

> Additionally it requires someone to meticulously compare the mathematical model with the implementation code, to validate that what is written actually maps to what was designed.

This is a deficiency in TLA+ (and many other systems), but it's not a good enough reason to discard or dismiss it. The industry alternative to TLA+ is not something that traces fully and easily from spec to code, but mostly to use informal, largely prose, documents as their specification (if they specify anything at all). TLA+ is a massive improvement on that even if it's not a perfect tool. Same for Alloy and other systems. It's better if people model and specify at least portions of their system formally even if it still takes effort to verify the code correctly implements that specification, effort they have to expend anyways but with greater difficulty lacking any thing approaching a formal specification.