The ION Language & Compiler

ION is a language designed to cater to principles of safety-critical, deterministic programming. The project's long term ambition is an attempt to shorten the distance from prototyping to certifiable high-assurance code. ION compiles to LLVM, and there may eventually be an Ada SPARK compilation target as well.

ION is in its early stages. Neither the language, nor the compiler, claim to be stable, safe or complete. Breaking changes may be introduced at any time.

from std.io import Logger
from sensor import (SensorReader, NoRecentDataAvailableError)

func makeSensorReader(): give SensorReader {
	ok new SensorReader()
}

export nofail func main(): void {
	var logger = new Logger[ascii?]()
	var sensorReader = take makeSensorReader()

	var position = sensorReader.readPosition() or {
		(error: NoRecentDataAvailableError) -> {
			logger.log("no sensor data received yet")
			ok nil
		}
	}

	logger.log("Position:")
	logger.log(position?.ascii())
}

Overview

ION is designed to cater to safe practices, many of which are also outlined by standards such as MISRA, DO-178 et al. Beside safety itself, this conservative approach also has the added benefit of reducing static analysis complexity. The language combines bounded numeric types, fully analyzed failure graphs and explicit affine ownership into a language that enforces safety at the cost of some verbosity and a restriction of cyclic data structures.

ION leans on concepts from SPARK Ada and similar languages, but also introduces new ideas, such as give/ take semantics for explicit ownership transfer, as well as the owner visibility keyword, making capability based programming more ergonomic. ION's design allows a deterministic heap memory model, without need for GC, ref-counting, etc.

Eventually, formal verification methods may be introduced as well, either through already existing toolchains like GNAT, or even gradual additions of formal methods to the ION toolchain itself.

Project Progress Overview

	Partially Working	Working	Correct & Safe
Language Design		✅
Semantics Analysis		✅
LLVM Backend	✅

Core Guidelines

All design decisions in ION are made based on a set of common guidelines. ION does not yet claim to fulfill all of these unequivocally, but aims to reach a state where these claims eventually all hold true:

• Explicit over Implicit
  Neither the programmer nor the compiler should have to infer semantic information from context. Instead, the language makes semantic information clearly visible in source code, interfaces and contracts. In other words: Transparency over Cleverness.
• Static Analysis over Runtime Checks
  If something cannot be proven safe at compile time, reject it, rather than deferring safety checks to runtime.
• Determinism over Ambiguity
  From high level control flow down to memory allocation, every possible operation in a program should be known at compile-time. Ideally, compiled programs are finite state machines.

License

Copyright (c) 2025, 2026 Fabian Lauer. All rights reserved. See full license text in LICENSE.txt.