Comment by hackingonempty

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.... https://www.youtube.com/watch?v=c3sOuEv0E2I