Hacker News Reader

We are! We very recently announced some results on formally proving the correctness of programs: https://harmonic.fun/news#blog-post-verina-bench-sota

Formal methods are cool because, by contrast to tools like the borrow checker, you can prove some very "nonlocal" properties: this system does not deadlock, or it makes progress at least every N steps, etc.

View on HN

Does Aristotle produce TLA+ output?

For example can it read rust async code and prove that there are no deadlocks in TLA+, or some equivalent in Lean?

TLA+ is generally used to specify a "toy model" of some complex distributed system. It's not intended for end-to-end proof, for that you'd just use Coq/Rocq or Lean itself. Lean is certainly expressive enough, but you'll have to translate the time and non-determinism modalities of TLA+ as part of the Lean development.

How is “this system doesn’t deadlock” not the same as the halting problem?

Proving that a particular program terminates does not require deciding the halting problem on arbitrary programs (same for deadlock freedom)

Deadlock is literally a halting problem.

We can't know for every possible program if it halts or not, but the complexity of programs we can determine is increasing as tools and techniques get better

Reply on news.ycombinator.com