How Are Programs Found? Speculating About Language Ergonomics With Curry-Howard

TL;DR

This paper explores the analogy between programs and proofs in functional languages with strong static types, suggesting that reliance on intuition and experimentation may hinder their practical adoption.

Contribution

It provides a speculative analysis linking mathematical proof practices to programming language ergonomics, highlighting potential reasons for limited real-world use.

Findings

Mathematicians value intuition and experimentation in proofs

Strongly typed functional languages may undervalue intuition

Practical challenges of rigorous languages are linked to human factors

Abstract

Functional languages with strong static type systems have beneficial properties to help ensure program correctness and reliability. Surprisingly, their practical significance in applications is low relative to other languages lacking in those dimensions. In this paper, the programs-as-proofs analogy is taken seriously to gain speculative insights by analysis of creation habits in the proof-centric discipline of mathematics. Viewed in light of this analogy, a sampling of mathematicians' attitudes towards formal proof suggests that the crucial role of intuition and experimentation in programming tasks may be under appreciated, hinting at a possible explanation of the challenges rigorously disciplined languages face in practical applications.