What's interesting about this view is that theorem provers ultimately boil down to sufficiently advanced type checking (the book Type Theory and Formal Proof is an excellent overview of this topic). Literally the heart of proof assistants like Lean is "if it compiles, you've proved it".
So more practical type systems can be viewed as "little" theorem provers in the sense the author is describing. "Thinking in types" so to speak, is mathematically equivalent to "writing little proofs in your head". I would also add that merely using types is not equivalent to "thinking in types" as one would be required to do writing a sufficiently advanced Haskell program.
It's true that theorem provers can be just sufficiently advanced type systems (the Curry Howard correspondence), but not all theorem provers operate that way. Isabelle/HOL operates on higher order logic. Imperative ones like SPARK or Dafny just rely on encoding preconditions and postconditions and things like loop invariants and just use SMT solvers for verification, IIRC.
Having an advanced type system does seem to encourage this sort of informal proof oriented thinking more than imperative and somewhat typeless languages do, though, since preconditions and postconditions and loop invariants and inductive proofs on loops are things you have to do yourself entirely in your head.