Aldela is a typed, denotational, and partially informal program design language. Its purpose is to let software designers express the structure of a system both prior to and in tandem with implementation - cleanly, precisely, and without being constrained by the quirks of any particular programming language.
Aldela is inspired by Conal Elliott’s Denotational Design and appends that with propositions, enabling a flexible blend of formal and informal specification.
Aldela is not a programming language. It has no compiler, no interpreter, and no runtime semantics. Instead, it is a pure design language with a parser and type‑checker that ensure structural correctness while leaving implementation concerns behind.
Modern systems-especially legacy systems-often have architectures that are:
- too complex to fully formalize,
- too important to leave undocumented,
- too brittle to redesign without a clear algebraic model.
Aldela provides a way to describe such systems using:
- Algebraic data types
- Typed lambda calculus (System Fω with type families and opt‑in subtyping)
- Categories (similar to type classes)
- Witnesses for category membership
- Natural‑language propositions
- Descriptions of intent
- High‑level architectural meaning
This dual approach lets designers choose the right level of precision for each part of a system.
- An algebraic design language
- A way to encode abstract program structure
- A tool for architecture, domain modeling, and system meaning
- A blend of formal types and informal propositions
- A language with a parser and type‑checker
- A programming language
- A runtime system
- A compiler or interpreter
- A verification system with dependent types
- An alternative to Agda or Coq
Aldela is about design, not execution.
Aldela aims to provide:
- A formal yet human‑readable language for describing software systems.
- A way to express design intent.
- A bridge between architecture, domain modeling, and implementation guidance.
This places Aldela in the same conceptual family as:
| Language / Framework | Similarity |
|---|---|
| UML | Structural modeling, diagrams |
| SysML | Systems engineering semantics |
| TLA+ | Formal specification, correctness |
| Alloy | Declarative modeling |
| Domain‑Driven Design | Ubiquitous language, domain structure |
| Architecture DSLs | High‑level system design |
Aldela unifies these ideas into a single, coherent design language.
Most tools fall into one of two buckets:
They force you to express your design in terms of execution, side effects, and implementation constraints.
They’re informal, untyped, and not machine-checkable.
However, Aldela gives you something that no other tool provides:
A way to formally and informally describe the meaning of a system’s architecture without being inhibited by implementation details.
Aldela sits in the middle:
This combination is unique.
Most large systems suffer from the same problems:
- The architecture exists only in people’s heads
- The codebase doesn’t reflect the intended design
- Documentation is incomplete or outdated
- Legacy systems can’t be fully formalized
- Implementation details distort the conceptual model
Aldela directly addresses these pain points.
It gives you:
Not the code. Not the runtime. Not the implementation. The architecture.
Because in software, the biggest failures aren’t caused by bad code - they’re caused by:
- unclear architecture
- mismatched mental models
- undocumented assumptions
- lost design intent
- accidental complexity
Aldela gives you a way to capture the meaning of a system so that:
- implementations can vary
- teams can align
- intent is preserved
- structure is explicit
- complexity is tamed
Aldela includes:
Natural‑language descriptions of meaning or intent.
Proposition "Convert a symbol to a string."
Proposition! "Attach debugger to code called inside the given container."
Products and sums, similar to ML/Haskell.
type Maybe<a> =
| Some of a
| None
Typed lambda expressions or propositions.
let symbolToString (s : Symbol) : String =
Proposition "Convert a symbol to string."
With optional constraints and witnesses.
category Monad<m; Applicative<m>> =
bind<a, b> : m<a> -> (a -> m<b>) -> m<b>
Provide implementations for category members.
witness Monad =
pure = vsyncReturn
map = vsyncMap
apply = vsyncApply
bind = vsyncBind
Aldela includes a full algebraic design for MetaFunctions, a system architecture intended to replace microservices.
type MetaFunction =
Provider -> Intent -> Symbol -> Vsync<Symbol>
let call (mfn : MetaFunction) provider intent args =
mfn provider intent args
This example demonstrates how Aldela can describe complex distributed systems using a mix of formal types and informal propositions.
Aldela is currently:
- Actively designed
- Partially implemented
- Open to feedback and contributions
The parser and type‑checker are under development.