[arka2147483647]

> Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way.

It sounds like what you think as positives are exactly the things parent comment thinks as negatives.

[agentcoops]

I used to work in this field myself long ago (academically and practically). The difficulty that OP didn't suggest much appreciation for is that the interesting spaces for automated verification -- especially of distributed systems, say -- require exploring the space of formalisms between the trivial proofs of propositional logic (SAT solvers) and the undecidable proofs of first or second-order logic (interactive theorem proving environments such as Isabelle and Lean). This is the incredibly large space occupied most importantly by the various modal logics, which allow for quantification over graph traversals. There are remarkably expressive logics where the decision problem remains tractable, such as the modal mu-calculus.

That is, precisely if one wants automated tools for verification the seemingly obtuse work on novel formal systems is necessary.

[ajb]

There's a big difference between wanting a succinct proof and wanting a succinct statement of the requirements. The easier it is to state the requirements, the more likely you have stated them correctly. Whereas succinct proof is not relevant for industrial purposes, as long as the proover has a small trusted kernel, it makes no difference to the reliability.