Programming Languages as Tools for Reasoning

Gordon, Colin S.

Oxford Handbook of Philosophy in Computer Science, November 2026

Abstract

Programming languages are designed for a wide variety of stated reasons, including examples such as simplifying concurrent programming; being easy to read, write, or learn; being more secure; supporting low-level systems programming; or being easy to reason about. This chapter articulates the position that all of the stated reasons for designing a new programming language in fact reduce to variants of the last: programming languages are designed primarily to support goals of reasoning about program behavior, differing primarily in who (or what) is performing the reasoning, the style of reasoning to be supported (what concepts are taken as primitive and what logical reasoning principles are assumed), and how that reasoning is intended to be performed (manually, automatically, or differently depending on the desired property). This chapter draws out connections between the design of programming languages and philosophy of logic (and to a lesser extent language). Many of the facets of program behaviour which language designers concern themselves with have close connections to other philosophical investigations of reasoning, which we demonstrate through overviews and more detailed examples of language design addressing several reasoning challenges, both well-known and lesser known.

Bibtex

@incollection{handbookPhilCS,
	bibtex_show = {true},
	abbr = {OUP},
	author = {Gordon, Colin S.},
	title = {Programming Languages as Tools for Reasoning},
	booktitle = {{Oxford Handbook of Philosophy in Computer Science}},
	editors = {Turner, Ray and Angius, Nicola and Stephanou, Henri},
	year = {2026},
	note = "Invited Contribution. To Appear..",
	abstract = { Programming languages are designed for a wide variety of stated
	            reasons, including examples such as simplifying concurrent
	            programming; being easy to read, write, or learn; being more
	            secure; supporting low-level systems programming; or being easy
	            to reason about. This chapter articulates the position that all
	            of the stated reasons for designing a new programming language in
	            fact reduce to variants of the last: programming languages are
	            designed primarily to support goals of reasoning about program
	            behavior, differing primarily in who (or what) is performing the
	            reasoning, the style of reasoning to be supported (what concepts
	            are taken as primitive and what logical reasoning principles are
	            assumed), and how that reasoning is intended to be performed
	            (manually, automatically, or differently depending on the desired
	            property). This chapter draws out connections between the design
	            of programming languages and philosophy of logic (and to a lesser
	            extent language). Many of the facets of program behaviour which
	            language designers concern themselves with have close connections
	            to other philosophical investigations of reasoning, which we
	            demonstrate through overviews and more detailed examples of
	            language design addressing several reasoning challenges, both
	            well-known and lesser known. },
}