>In Idris, you've typed your types. I've always typed not only my types, but functions, programs, tests, everything, in every language I've ever coded in. OK,

>In Idris, you've typed your types. I've always typed not only my types, but functions, programs, tests, everything, in every language I've ever coded in. OK, sometimes I first write stuff (in pseudocode, or at least bad syntax) on paper first, but in the end I always type it into a code editor on the computer. Type type type, clickety click click clack...