Not so drab -- that sort of thinking can lead to a pretty big deal, namely, the Curry-Howard Isomorphism[0]. From the linked WP page: In other words, the Cur

Not so drab -- that sort of thinking can lead to a pretty big deal, namely, the Curry-Howard Isomorphism[0]. From the linked WP page: In other words, the Curry–Howard correspondence is the observation that two families of formalisms that had seemed unrelated—namely, the proof systems on one hand, and the models of computation on the other—were, in the two examples considered by Curry and Howard, in fact structurally the same kind of objects. If one now abstracts on the peculiarities of this or that formalism, the immediate generalization is the following claim: a proof is a program, the formula it proves is a type for the program. More informally, this can be seen as an analogy that states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem ... and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run. (Of course, in the context of those job interviews you mentioned, this sort of thing would probably be overkill, unless the job involved functional-programming...in which case, though, they might well not have asked you how your "skills in mathematics would transition to programming" in the first place :-) ). [0] https://en.wikipedia.org/wiki/Curry–Howard_correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence