A mathematician that has only used a type theory like Coq or Agda and never Haskell.