In the footnote, the author linkedly suggests to "Read That F* Code".

Indeed, it is good to be able to read F* code.

So not sure why the author does suggest to be Typer and Thinker at same time. Thinking in Types(and categories) composes well with traditional logical thinking imho.