---
title: "Constructive Mathematics and Computer Programming"
authors:
  - "Per Martin-Löf"
year: 1982
venue: "Logic, Methodology and Philosophy of Science VI"
arxiv: null
doi: "10.1016/S0049-237X(09)70189-2"
source: "https://doi.org/10.1016/S0049-237X(09)70189-2"
topics:
  - martin-lof
  - type-theory
  - constructive-math
  - programming
seed_rank: 649
seed_batch: "perfects-pl-2026-08-13"
reviewed: "2026-08-13"
pool: "languages"
relevance_score: 10
lineage: programming-language-foundations
cites:
  - title: "An Intuitionistic Theory of Types: Predicative Part"
    url: "https://doi.org/10.1016/S0049-237X(08)71945-1"
    year: 1975
    arxiv: null
    doi: "10.1016/S0049-237X(08)71945-1"
  - title: "The Formulae-as-Types Notion of Construction"
    url: "https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf"
    year: 1980
    arxiv: null
    doi: null
see:
  - "648-an-intuitionistic-theory-of-types-predicative-part"
  - "647-the-formulae-as-types-notion-of-construction"
---

# Constructive Mathematics and Computer Programming

## One-sentence takeaway

Martin-Löf argues that constructive type theory *is* a programming language: a proof of a specification is a program, and running it is proof reduction.

## Why it matters here

The manifesto that programming = proof construction — the reason Broadside keeps type theory next to PL and why an ano specification could in principle be inhabited by a checked term.

## Key ideas

- A specification is a type; a program meeting it is a term of that type.
- Computational content of intuitionistic logic is exactly the reduction behaviour of the corresponding typed terms.
- Type theory is offered as a wide-spectrum language, from machine-near combinators to mathematical constructions.
- *LMPS VI* (Hannover 1979 / North-Holland 1982). Influences Coq/Agda/Nuprl cultures of program extraction.

## Caveats

## Links

- DOI: [10.1016/S0049-237X(09)70189-2](https://doi.org/10.1016/S0049-237X(09)70189-2)