I would imagine an idris derivative isnt all that much easier to write when compared with writing coq.

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.

Are we not confusing difficulty with familiarity? For me personally, as someone very familiar with FP, Idris was very approachable and easy to at least write simple proofs in.

I have nothing to say about the language (I gave up reading those cumbersome slides), but I am really amazed that you expect someone to like that presentation! :)

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.