Engineering the
Last Programming Language

Dream unifies formal verification, automatic parallelism, content-addressable code, and AI-native design into one coherent language.

The Book Learn More 
fn transfer(
  πŸ™ from: Account,
  πŸ™ to:   Account,
  amount: v: Nat | v > 0
) with [Transaction, Log] β†’ Result⟨Receipt, TransferError⟩

Five Pillars

Every feature in Dream exists because of a real problem that current languages fail to solve.

Verification

Quantitative types, refinement types, and SMT-backed proofs β€” from prototype to proof with the ? operator.

Parallelism

Interaction combinators give you automatic GPU parallelism for pure code β€” no threads, no locks, no data races.

Code Identity

Content-addressable definitions β€” no more dependency hell. Code is identified by what it does, not where it lives.

Effects

Algebraic effects with row polymorphism β€” composable, typed side effects that make testing and reasoning effortless.

AI-Native

Compiler-as-library, typed holes, constrained decoding, structured errors β€” designed for AI to read and write.

A Taste of Dream

Linear Resources
fn send(πŸ™ msg: Message) β†’ Receipt
// msg must be used exactly once
// compiler enforces: no copies, no drops
State Machines
machine Door 
  state Locked, Unlocked, Open
  Locked  β†’ Unlocked via unlock(key)
  Unlocked β†’ Open    via push()
Gradual Verification
// Start unverified, add proofs later
fn sort(xs: List⟨Int⟩)
  β†’ r: List⟨Int⟩ | sorted(r) ∧ perm(r, xs)
  = mergeSort(xs) trust ?
The Book
Dream
Engineering the Last
Programming Language
22 chapters · 4 appendices

The Book

A deep dive into language design β€” from quantitative type theory and interaction nets to algebraic effects and AI-native compilation. Not a tutorial. A blueprint for the future of programming.

  • Part I The Problem
  • Part II The Dream
  • Part III The Type System
  • Part IV Execution Models
  • Part V Verification
  • Part VI–XI Infrastructure, Systems, Research…
In progress — early access coming soon
Get Notified

Stay in the Loop

Be the first to know when early access opens. No spam β€” just milestones.

We'll connect this to a mailing list once the site goes live. For now, this is a placeholder.