[Tarean]

I notice that I have two modes of programming. This is clearest with haskell.

For simple code I make type errors into runtime errors and let the compiler figure out type signatures. This emulates dynamic languages with a great linter pretty well.

For complex code I write rigid type signatures first and then play type tetris. This works best with dependently typed languages and is called type driven development. Idris can fill in large parts of the program with this - since type signatures are equivalent to propositions and programs to proofs this is basically proof search.