Stellogen

A programming language where computation and types are built from the same mechanism: term unification.

Stellogen is a research language exploring what programming looks like without primitive types or fixed logical rules, just elementary interactive building blocks based on term unification.

Status: Experimental proof of concept / Research project / Esoteric language (not production-ready)

---

Why Stellogen?

Traditional typed languages use types to constrain programs and ensure correctness. Types act as questions, programs as answers. This is powerful but also constraining, it defines which questions you can even ask.

Stellogen explores a different path:

• Computation and typing use the same mechanism (term unification)
• No primitive types or fixed logic imposed from above
• The compiler only checks that blocks connect: semantic power belongs to you

This shifts responsibility from the language designer to the user. With that power comes the need for discipline, but also the freedom to explore computational models that don't fit traditional type systems.

Influences

Stellogen draws inspiration from:

• Prolog/Datalog - Unification and logic programming
• Smalltalk - Minimalism and message-passing
• Rocq (Coq) - Proof-as-program paradigm
• Scheme/Racket - Metaprogramming philosophy
• Shen - Optional type systems and user responsibility
• Girard's Transcendental Syntax - Theoretical foundation

What Makes Stellogen Different?

• No primitive types - Types are user-defined as sets of interactive tests
• Unification everywhere - The same mechanism handles both computation and type checking
• Logic-agnostic - Build your own logic rather than conforming to one imposed by the language
• Multi-paradigm - Express logic programming, functional, imperative, or OO styles using the same underlying mechanism

Stellogen's constellation-based model supports multiple programming paradigms:

---

Quick Example

; Define variable x as positive first-order term +f(a)
(def x (+f a))

; Define variable y as block of terms containing +f(X) and X
(def y [(-f X) X])

; Display [(-f X) X] on screen
(show #y)

; Make x and y interact along (+f a) and (-f X)
; The conflict is resolved and propagated to the other term X
; It results in [a]
(def result (exec #x #y))

; Display result [a] on screen
(show #result)

---

Getting Started

1. Install

Option A: Download Binary (fastest)

• Get the latest release from Releases then put the executable in your PATH as sgen.

Option B: Install via opam (up-to-date and more convenient)

opam pin stellogen https://github.com/engboris/stellogen.git
# The command sgen is directly accessible from your PATH

Option C: Build from Source

# Install dependencies
opam install . --deps-only --with-test

# Build
dune build

# Executable will be in _build/default/bin/
# You can put it in your PATH for more convenience

Option D: Build with Nix

nix build

If you wish, you can explicitly specify the derivation, like nix build .#default:

• default/stellogen: The default binary
• stellogen-minimal: Minimal version without documentation and JavaScript
• stellogen-web: JavaScript version
• playground: Playground files you can host with e.g. python3 -m http.server or directly with nix run .#playground
• docs: Documentation

2. Run Your First Program

Assuming the executable is named sgen and that it is in your PATH:

sgen eval examples/hello.sg

3. Learn the Basics

• Quick tutorial: https://github.com/engboris/stellogen/wiki/Basics-of-Stellogen
• Examples: Explore examples/ directory

---

Commands

Stellogen provides five main commands:

eval - Evaluate a Program

Evaluate both phases of a program, the check phase first and the run phase only if it passed. This is the normal way to invoke a Stellogen file:

sgen eval <filename>

Example:

sgen eval examples/hello.sg

A failing assertion means the run phase is never attempted.

run - Run Phase Only

Execute the run phase, skipping every check:

sgen run <filename>

Since nothing at runtime verifies that checking ever happened, a program shipped this way needs sgen check to have passed first.

check - Check Phase Only

Evaluate the check phase alone: specifications, § items and the type assertions written with ::. This is what a CI gate runs.

sgen check <filename>

preprocess - View Preprocessed Code

Show how macros expand and code is preprocessed:

sgen preprocess <filename>

Useful for debugging macro expansions and understanding how syntactic sugar is desugared.

trace - Interactive Execution Trace

Step through program execution and visualize how stars interact:

sgen trace <filename>

Shows each fusion step with visual arrows pointing to the exact rays being connected. Press Enter to advance through each step.

For re-running on file changes during development, use a general-purpose watcher such as entr or watchexec, e.g. ls myprogram.sg | entr sgen eval myprogram.sg.

---

Ready to explore? Dive into the Quick Tutorial!