Yes, I have that quirk too. I try to push it down, because sometimes I just need to get something done. I like using J/APL composing functions which keeps it all in my head and I don't need types at that level. I have played with Agda, Coq, and Idris, but I always feel a pull to Haskell. SPARK2014 has a lot going for it, and I am trying to use it to create a controls program utilizing a lot of its inherent features for safety and integrity. ATS seems to hit a lot of notes too. At the end of the day, I feel more playful and enjoy programming in Lisp and J or APL, which is why April really caught my attention. I am learning BQN, but the symbols are not jiving with me personally; I prefer APL's symbols. BQN's symbols seem to all look slightly similar whereas APL symbols seem geometrically different enough and they suit my aesthetic. Let's see in another 3 months!