Hacker News Reader

What about a better interface for Coq? I think this makes more sense to experienced programmers. Also for mankind.

I agree. One could argue that Agda and Idris are a better interface to the type theory that underlies Coq.