iota - design

This is a draft design for a programming language/environment.


A low-level language aiming to be small and principled:

  • A limited, ascetic and opinionated set of language features. Unambiguous, simple, minimalistic syntax; context-free grammar. Still richer than Forth/Lisp/Smalltalk.
  • Having data notation, generic maps, nested dot-namespaces and context-aware completion is a must.
  • Make everything (threads, stacks, allocators, effects, assumptions) as explicit as possible, while keeping it not too verbose. Capabilities and contexts instead of ambient authority.
  • But: try to keep complexity gradual, scale down.
  • Reifies abstractions from full linear/ordered dependent typing to the actual bare-metal bytes manipulation. Nothing should be forced to be unsafe at any possible level of compilation or execution, as long as you can or want to prove safety.
  • Everything that happens at runtime can be reflected on. A systems language is more than just a compiler blueprint. Every bit of data is transparent, structured and accounted for. Its meaning can be erased only explicitly.
  • Think about async, fallibility and diagnostics upfront.


Progressive enrichment of semantics, staged run-time:

  • ground layer: plain text.
  • data layer: a notation/model for data (like EDN for Clojure). It's map-structured with additional amenities for Lean-style functional programming (think JSON/S-expressions, but rich just enough to write actual code, austerely).
  • schema layer: adding some rudimentary typing/schemas on top of data layer. Suitable for configs/serialization. Data should be usable both in-memory and when streamed somewhere else.
  • lambda layer: a Calculus of Inductive Constructions semantics able to encode Lean-style proofs. It is built on top of the data layer by adding grammar restrictions and executable/CoIC semantics. Resource management is not a concern.
  • systems layer: linearly/ordered-typed modification of lambda layer that is concerned with resource management (memory: allocations, references, borrow checking; input/output, async, threads). Can be compiled to a standalone executable, fast and close to metal, with the runtime environment still retaining a lot of metainformation and providing good reflection and dynamic linking (fatter than Rust, slimmer than Go runtime).


  • Lean: proofs, properties, standard library, syntax?
  • Clojure: data notations, maps, rich homoiconicity.
  • Swift: witness tables, layout-agnostic structs, dynamic runtime.
  • Golang: syntax, syntactic minimalism
  • Rust: safe memory/resource management, traits, namespaces
  • Zig: compile-time evaluation, explicit allocators.
  • Austral: linear types, capabilities, runtime minimalism