Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

About

This book distills a way of thinking about software inspired by Conal Elliott’s Denotational Design. The core idea is simple yet profound:

Denotational Design

Define the meaning of a program before deciding how it runs.

In this view, computation is not an opaque sequence of steps but a transparent mathematical object. We begin with specifications as pure, compositional descriptions of what a program means. These are expressed as algebraic structures, often in the form of traits or type signatures. The implementation, how those meanings are realized, is a separate, interchangeable layer.

By separating meaning from mechanics, we gain:

  • Clarity - programs read like precise definitions.
  • Composability - parts fit together algebraically.
  • Refactorability - meaning stays fixed while implementation evolves.
  • Correctness - reasoning about programs becomes equational, not operational.

These guidelines aim to provide practical techniques for applying this style in modern programming languages, especially Rust, without losing the elegance and rigor of its mathematical roots.

Reference of mdbook

mdBook documentation

Reference of admonish mdbook plugin (tooltip boxes)

admonish documentation