It's wonderful to see an article about this topic that's grounded in rigorous thought. And that references the long, rich history of folks who have worked hard to articulate the problems and solutions one encounters when programming.

From my experience and training, I'm biased towards the Church-style of thought for representing all programs. My reasoning is simple: ultimately, we write programs to solve a problem. The implementation of the program is a secondary concern to producing a correct solution. An incorrect solution is just about as useful as a program that immediately exits after starting. [1]

Using the type-oriented perspective to programming shifts the paradigm from *how* a computer program works to *what* it is accomplishing. When we're sure we have the "what" correct, we can then perform transformations on our program to optimize its implementation to achieve different second-order properties on the "how." Do we need this to run faster? Do we need this to use less memory? Do we need this to re-use a pool of threads or network connections? Do we need this to use SIMD instructions because that's what our hardware supports? The possibilities for "how" can be seemingly endless: they're always use-case specific.

However, when we're thinking about solutions, we necessarily must be focused on achieving a singular goal: the problem is solved. When we use types to represent our program semantics, we gain an awesome level of problem-solving ability. We can ensure that our program semantics really do solve our problem. We don't need to wait for an actual execution of our program to determine whether or not we've solved it. In a laymen's sense of the term, we gain an exponential speed-up in our ability to make correct programs. It makes insanely complex problems solvable. And it makes the simple ones trivial.

We stop wasting our time focusing on re-solving every detail that needs to go into the execution of our program. Instead, we are able to build upon foundations that _we know work_. Could we get to where we are today if we had to to write every new program in hardware-specific assembly? Implement every piece of functionality going down to the level of "how will my processor be able to execute this?" Of course not! We've realized this in many cases: when we use compilers, we transform a solution defined in one space to an equivalent solution defined in another; we implement our web app endpoints using the types and semantics of WSGI; we make our complex distributed systems on the back of infrastructure with well-documented components that specify the types of things that they support and what they provide. We're surrounded by examples of successful large systems that rely explicitly on defining types.

Ultimately, it's my strongly held belief that for the software industry to mature to genuine engineering, it's imperative for our collective thought to embrace mathematical rigor. This is not to gatekeeper others: everyone can learn. We must believe that we can understand this well enough to teach absolutely _anyone_ who is willing to put in the time and effort to understand.

If we're serious, we need to graduate from the notion that we're only writing programs to we're coding up solutions to our problems. Where we define and reason about the problem at a conceptual, abstract level and then move towards reusing and combining solutions from Computer Science.

--

[1] And it may be _less useful_ than that: consider a program that produces _ever so slightly wrong_ results. Is it feasible to always verify that its output is always correct _each time that it is run_? If one needs to do that work, then is it actually automated? If it's not automated, why put in the effort to program a machine to perform the work?