Comment by nextos | Hacker News Reader

Comment by nextos | Hacker News Reader

Parent Full thread

I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. 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. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like LTL or, more recently, separation logic, have been incredible breakthroughs.

TLA+, which has gained quite a lot of popularity, is a testament to that. Model checking is eminently practical. The exciting thing now is that heavier formal methods, in particular theorem proving, might become cheap enough to use in regular systems software. Writing formal specifications for functions and getting them synthesized and proven correct by some SAT/SMT, theorem prover & LLM hybrid may become the norm in the not-too-distant future.

[1] On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf

[2] From Philosophical to Industrial Logics. https://www.cs.rice.edu/~vardi/papers/icla09.pdf

Thanks for the pointers to the papers.

One book which seems not that well known is Arindama Singh's Logics for Computer Science 2nd edition - https://www.phindia.com/Books/BookDetail/9789387472433/LOGIC...

For more details see author's webpage - https://home.iitm.ac.in/asingh/books.html

> 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.

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.

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.

"Logic is to computer science and software engineering what calculus is to ... mechanical or civil engineering"

Things professionals rarely use in practice?

> TLA+, which has gained quite a lot of popularity

Why do you think that? Outside of just toy examples, and vague examples of "AWS uses that", I don't know of any actual code which has TLA. Most of the things you can do with TLA, you can do with informal math notation quite easily.

Do you have any real world long term usage examples?

See for example https://www.mongodb.com/company/blog/engineering/conformance...

We have a number of TLA+ models at Oxide. Here's one:

https://github.com/oxidecomputer/omicron/blob/8b0886dbd02229...

Reply on news.ycombinator.com