7 ms·
We are! We very recently announced some results on formally proving the correctness of programs: https://harmonic.fun/news#blog-post-verina-bench-sota https://h
by maxwells-daemon 8mo 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 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.
- vatsachak 8mo agoDoes 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?
- zozbot234 8mo agoTLA+ 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.
- NetMageSCW 8mo agoHow is “this system doesn’t deadlock” not the same as the halting problem?
- pvillano 8mo agoDeadlock 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
- xjm 8mo agoProving that a particular program terminates does not require deciding the halting problem on arbitrary programs (same for deadlock freedom)