4 ms·

Thank you for the write-down, it is very interesting! Is there some reason why Rocq is the proof assistant of choice and not one of the others? also.... htt

• nathanrf 1y ago
  It is as simple as: the person who contributed the proofs/implementations chose Rocq. I did some small proofs in Dafny for a few of the simpler deciders (most of which didn't end up being used). At the time, I found Dafny's "program extraction" (i.e. transpilation to a "real" programming language) very cumbersome, and produced extremely inefficient code. I think since then, a much improved Rust target has been implemented.
• LegionMammal978 1y ago
  Its focus around constructible objects does lend itself well to the kind of proofs needed for non-halting. Usually they involve lemmas about the 'syntax' of a TM's configuration and how it evolves over time, and the actual number-based math is relatively simple. (With the exception of Skelet #17, which involves fiddly invariants of finite sequences.)