Haskell programming is often "conversations with the type checker".
The more I enjoy this process of talking to the type checker, the more I get the urge to dive into Agda.
I've heard from several people who do all their design work in the Agda type system, and rarely execute the resulting code.
That sounds like fun?
Are there more/other tools that encourage/allow "conversations with correctness" ?
I do that in Haskell with type holes, etc.
I hear Agda is designed for this?
Dan Piponi says C++ "concepts" do that.
Is incremental typing a member of that set?
Do you know of more?
