I would change it a bit. Lambda calculus (in Martin-Lof type theory) are Maxwell equations of logic. But, lambda calculus has very little real use in programmin

I would change it a bit. Lambda calculus (in Martin-Lof type theory) are Maxwell equations of logic. But, lambda calculus has very little real use in programming. There should be something else here.