Arguably computing as a discipline is an important part of what makes contemporary lifestyles possible, and most of it, especially the practical parts, resembles the liberal arts more than it resembles mathematics. Especially areas like programming languages overall operate more through argumentation and analogy than through proofs. Sure, there are subsidiary proofs involved that can tell you something useful about the building blocks, but the type-related theorems you find in appendices of POPL papers are just low-level machinery, not the real goal, which is a usable programming language that people can do real work with. That requires constructing an overall language and ecosystem through a pretty liberal-arts style methodology: looking at what worked previously, reasoning what went well and badly about that, critically considering illustrative examples (often carefully constructed examples designed to illustrate a point, similar to the thought experiments in philosophy), and attempting to improve things on the basis of all that. If you look at a Rich Hickey talk, for example, that's pretty much entirely how he proceeds. And even in POPL papers, that's what you find in the meat of most influential papers (as opposed to the appendices): the real result of an influential paper is typically a qualitative argument about programming constructs, where the argument is convincing and well supported by examples, by not "proven" in any mathematical sense.
