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