Comment by maxwells-daemon
2 days ago
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.
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?
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
Proving that a particular program terminates does not require deciding the halting problem on arbitrary programs (same for deadlock freedom)