Yeah, I'd attribute this to the lambda calculus, for sure. And in the lambda calculus, it makes a ton of sense, because it allows you to break proofs into smal

Yeah, I'd attribute this to the lambda calculus, for sure. And in the lambda calculus, it makes a ton of sense, because it allows you to break proofs into smaller chunks more easily. But in a general-purpose programming language where the proofs are automated, I think this just makes the code less communicative of programmer intent.