Most of programming is done in something reminiscent of type theory. Actual languages are more complicated because they either are impure (C, C++ etc) or involve non-total functions (Haskell). Idris, Coq and Agda can be reduced to some sort of type theory.

On the other hand, most of mathematics can be done in first order logic (FOL).

As for English, I'm not much of a linguist but I believe the closest equivalent to the above for English (and other natural languages) would be Categorical Grammar or maybe Montague grammar.