Oh yeah, Ive known people who could do model checking giving up on Idris since it was too difficult. What's interesting about Noether is it builds up from simplest models of computation to single threaded to distributed. The lower levels are like state machines. One could do that in languages for contracts working up from brute-forceable automata toward more expressive stuff that takes more work.

Plus, I thought you'd enjoy the language presentation as extra benefit.

Proving theorems in Agda or Idris is like programming in more rigorous variant of Haskell. Proving theorems in Coq is... different.

I agree.

I do proofs and write small programs in coq regularly. I've spent most of my professional life as a web developer.

As with everything learning to do proofs and learning to use Coq are a matter of time, effort, and access to good documentation and other resources.