The Inference Programming Language

Warning

The Inference programming language is currently under development. If you see this message, it means that the first stable release is not out yet. However, this book describes the current state of the language and currently available features. Therefore, feel free to explore and try out Inference!

To follow updates about the language and its development, follow the dev team’s official social media channels ・・・

We welcome contributions from the community. You can help improve Inference by trying out the language and sharing your experience, providing feedback on language features and design decisions, reporting implementation bugs, suggesting improvements to this documentation, or discussing new features on our Discord. Your input helps shape the development of Inference.

Foreword

Software correctness is a cornerstone of reliable computing systems. As humanity invents and develops more sophisticated and immersive technologies, the demand for resilient software that behaves exactly as intended has become increasingly critical. We have always had systems that must never fail because their real-world side effects are irreversible by nature. For example, nuclear power plant control software should never drain coolant from a reactor, and cars must never deploy airbags at highway speeds when no collision occurred.

The Inference project started in January 2023 to address the challenges that this new era of computing brings. With the advent of blockchain and cryptographic protocols, quantum computing, AI-managed systems, and robotics, the need for software that is provably correct and secure has never been more pressing. No one wants a household robot to decide to iron clothes that are currently being worn by someone. Likewise, smart contract exploits do more than just drain funds, they hinder the evolution of financial systems.

Traditional testing and debugging methods, while useful, often fall short of providing absolute guarantees about program behavior. Formal Verification (FV), despite being one of the most advanced and reliable techniques for ensuring the correctness of algorithm implementations, has for decades been underrepresented and used primarily in aerospace, military, and other safety-critical industries.

Inference aims to bring Formal Verification into the software engineering mainstream.

Introduction

You are reading a book about The Inference Programming Language. With Inference, you can write highly reliable, mission-critical programs with a high level of confidence that they will behave exactly as intended. Inference is designed from the ground up to support formal verification (FV) of program properties, allowing you to prove code correctness mathematically with machine-checked proofs of behavior without needing to learn complex mathematical theories or specialized verification tools. Inference lets you write programs and their specifications in the same language and even in the same file, much like you would do with unit tests.

Who Inference Is For

The key power of Inference is that it has formal verification built-in from the start. Therefore, Inference is best suited for developing high assurance software. Here are some groups of people who will benefit the most from using Inference.

Developer Teams

Inference provides a way to rigorously ensure the correctness of code through formal verification. For development teams working on mission-critical applications, this means they can obtain mathematical guarantees that specified properties of their programs always hold, rather than relying solely on testing and code review. This leads to substantially lower residual defect risk, higher quality software, increased reliability, and improved safety of its users.

Examples of such software include, but are not limited to:

• Cryptographic software and security systems
• Various vehicle control systems (e.g., automotive, aerospace, marine)
• Medical devices and healthcare software
• Design and production of chips and circuits
• Blockchain, financial systems and banking software
• Industrial automation and control systems

Researchers

Traditionally, formal verification has been a complex and specialized field, requiring deep knowledge of mathematical theories and specialized tools. Most of the existing formal verification tools are used by experts from academia and research institutions. Inference lowers the barrier of entry for researchers and provides a unified platform for writing and verifying code, making it easier to explore new ideas and push the boundaries of what is possible with formal verification.

Students

Students learning computer science can benefit from using Inference to gain a deeper understanding of programming languages, mathematical logic, reasoning, and formal verification concepts. By using Inference, students can learn how to write correct and reliable code from the start, developing good programming habits that will serve them well in their future careers.

People Who Value Reliability and Safety

Inference is an excellent choice for anyone who values reliability and safety in their software. Whether you are developing software for personal use or an open source library for a larger audience, Inference provides a way to ensure that your code behaves as intended and meets the highest standards of quality and reliability.

Who This Book Is For

This book assumes that you are already familiar with at least one programming language with systems-programming capabilities. However, no prior knowledge of formal verification or mathematical logic is required. The book will guide you through the key concepts of the Inference programming language and its formal verification capabilities, providing practical examples and exercises to help you learn by doing.

Common programming concepts will not be covered in depth, but sufficient explanations and examples will be provided to help you get started quickly.

New concepts and semantics specific to Inference will be explained thoroughly, with a sufficient amount of detail and examples.

How to Use This Book

Read this book in the order it is presented, from start to finish. Each chapter builds upon the previous one and newly introduced concepts will be used in the subsequent chapters.

Additional resources and references are provided in the appendix section for further reading and exploration. The infs CLI Reference appendix provides a complete guide to the toolchain manager.

Source Code

The source files from which this book is generated can be found on GitHub.

Getting Started

In this chapter, we will discuss the following topics:

• Installing Inference on Linux, macOS, and Windows
• Writing a program that returns a mysterious number 42

Installation

To install Inference you need to download the compiler binary for your operating system from the infc GitHub Releases page.

Command Line Notation

In this book, commands you should type in a terminal start with $. Do not type the $ itself; it is just the prompt. Lines without $ show the output of the previous command. PowerShell examples use > instead of $.

Downloading the Compiler

Tip

If you prefer automated installation with PATH configuration, use the infs toolchain manager instead: infs install. See Appendix D - infs CLI Reference for details.

The Inference compiler (infc) is distributed as a single standalone binary with no external dependencies. It compiles Inference source code directly to WebAssembly without requiring any additional tools for compilation.

Download the appropriate package for your operating system from the GitHub Releases page.

Installing on Linux and macOS

Download the release archive, extract it, and you will find the infc binary:

$ tar xzf infc-linux-x64.tar.gz

Installing on Windows

Download the zip archive and extract it. You will find the infc.exe binary. No additional libraries or dependencies are required.

Package Contents

After extracting the archive, you will have:

infc            (or infc.exe on Windows)

That’s it — just the compiler binary. The Inference compiler generates WebAssembly modules directly, with no external toolchain needed.

Verifying the Download

To verify the integrity of the downloaded package, check its SHA256 checksum. The checksum is listed on the GitHub Releases page.

On Linux/macOS:

$ sha256sum infc-linux-x64.tar.gz

On Windows:

> Get-FileHash infc-windows-x64.zip -Algorithm SHA256

Adding infc to your PATH

On Linux/macOS, add the following line to your shell configuration file (e.g., ~/.bashrc, ~/.zshrc):

$ export PATH=$PATH:/path/to/infc-directory

On Windows, run the following command in PowerShell:

> $env:Path += ";C:\path\to\infc-directory"

Tip

If you use the infs toolchain manager, it handles PATH configuration automatically. See Appendix D - infs CLI Reference for details.

Installing a WebAssembly Runtime

To run compiled WebAssembly modules, you need a WASM runtime. This book uses wasmtime, a popular and easy-to-use runtime. Visit its official website for installation instructions.

Note

wasmtime is only needed if you want to execute compiled programs locally. The Inference compiler itself does not require it.

Editor Support

Inference has an official Visual Studio Code extension that provides syntax highlighting and language support. You can install it from the VS Code Marketplace or search for “Inference” in the VS Code extensions panel.

Verifying the Installation

Once installed, verify that the compiler is available:

$ infc --version
$ infs version

You should see the version printed in the terminal.

Hello World

Traditionally, the very first program you write when learning a new programming language is one that prints “Hello, World!” to the screen. In Inference, however, we do not have built-in string and printing functionality. Instead, we will write a simple program that returns a magic number from a function. Later, by executing this program, we will see the result in the terminal.

Writing the Program

First, we need to create a new file for our program. Inference uses the .inf file extension for its source code files. Create a new file named hello_world.inf and open it in your favorite text editor. Then, add the following code to the file:

pub fn hello_world() -> i32 {
    return 42;
}

This code defines a function named hello_world that takes no parameters and returns a 32-bit signed integer (i32). The function simply returns the number 42.

Understanding the Code

Let’s break down the code to understand its components:

• pub is a visibility keyword that marks the function as exported from the compiled WebAssembly module, making it callable from outside;
• fn is a keyword used to define a function in Inference;
• hello_world is the name of the function;
• () is a pair of parentheses that groups the function parameters. In this case, there are no parameters;
• -> reads as “right arrow” and indicates the return type of the function;
• i32 specifies that the function returns a 32-bit signed integer;
• return is a keyword used to return a value from a function;
• 42 is the integer value (or literal) being returned by the function.

In the appendix, Language Reference, you can find more information about Inference keywords and data types.

Compiling the Program

To compile an .inf file into a WebAssembly module, use the infs build command. Open your terminal, navigate to the directory where you saved hello_world.inf, and run the following command:

On Linux or macOS:

$ infs build hello_world.inf

On Windows:

> infs build hello_world.inf

The compiler will generate a WebAssembly binary module at out/hello_world.wasm.

Note

You can also use the infc compiler directly as an alternative:

$ infc hello_world.inf

Both commands produce the same output.

Running the Program

To execute the compiled WebAssembly module, we can use any preferred Wasm runtime. In this example and throughout this book, we will use wasmtime, a popular and easy-to-use Wasm runtime. You can install and learn more about wasmtime from its official website.

Once you have wasmtime installed, you can run the compiled module using the following command:

On Linux or macOS:

$ wasmtime out/hello_world.wasm --invoke hello_world

On Windows:

> wasmtime out/hello_world.wasm --invoke hello_world

As a result, you will see the output 42 printed in the terminal, which is the value returned by the hello_world function.

Congratulations! You have successfully written, compiled, and executed your first Inference program. In the next chapters, we will explore more features of the Inference programming language.

Common Programming Concepts

This chapter covers common programming concepts that are shared across many programming languages. It does not focus on Inference-specific features. Instead, it presents Inference as a high-assurance, software-oriented programming language and introduces the core principles and syntax you need to write executables and libraries in Inference.

In this chapter, we cover data types, variables and mutability, functions, and comments. Understanding these concepts is essential for writing programs in Inference.

The chapters that follow will build on these concepts with expressions and operators, control flow, and arrays.

Inference keywords, data types, and other language constructs are covered in the Language Reference appendix.

Data Types

Inference is a statically typed language — every value and variable must have a known type at compile time.

Integer Types

Inference supports both signed and unsigned integer types:

let small: i8 = 127;
let byte: u8 = 255;
let number: i32 = 42;
let big: i64 = 1000000;
let positive: u32 = 0;

i32 is the most common integer type and maps directly to a 32-bit integer in WebAssembly.

Boolean Type

let flag: bool = true;
let done: bool = false;

Array Type

Fixed-size arrays are written as [T; N], where T is the element type and N is a compile-time constant:

let numbers: [i32; 3] = [1, 2, 3];

See Arrays for full coverage.

Struct Type

User-defined types with named fields:

struct Point {
    x: i32;
    y: i32;
}

let p: Point = Point { x: 10, y: 20 };

Structs support methods via impl blocks — see Functions for details.

Enum Type

A type with a fixed set of named variants:

enum Color { Red, Green, Blue }

let c: Color = Color::Red;

See Enums for full coverage.

Floating-Point Types

Inference does not support floating-point types. It uses integer arithmetic to ensure determinism and precision in computations.

Variables and Mutability

Variables

Variables are declared with let, and require a type annotation and an initial value:

let x: i32 = 42;
let flag: bool = true;

Inference does not infer types — every variable must have an explicit type annotation.

Immutability by Default

Variables are immutable by default. Use let mut to allow reassignment:

let x: i32 = 5;
// x = 6;  // compiler error: x is not mutable

let mut y: i32 = 5;
y = 6;  // OK

Constants

Constants are declared with const and must be initialized with a literal value:

const MAX_SIZE: i32 = 100;
const THRESHOLD: i64 = 50000;
const ENABLED: bool = true;

Functions

A program is a sequence of instructions (or operations) that the computer executes to perform a specific task. Conceptually, a program is a function: it takes some input and produces some output. To write complex programs, we use functions as building blocks to decompose a program into smaller, manageable pieces. Similarly, libraries provide reusable functions that can be called from different programs. The Inference programming language is all about writing functions. As we saw in Hello World, the smallest Inference program is a function.

Anatomy of a Function

pub fn function_name(param1: Type1, param2: Type2) -> ReturnType {
    // function body
}

• pub makes the function exported from the compiled WebAssembly module. Without pub, a function is private to the file.
• -> ReturnType declares the return type. Functions without it return nothing.
• return is required to return a value — there are no implicit returns.

Parameters

Each parameter has a name and a type annotation:

pub fn add(a: i32, b: i32) -> i32 {
    return a + b;
}

Parameters are immutable by default. Declare with mut to allow modification inside the function body. All values are passed by copy — mutating a parameter does not affect the caller:

pub fn increment_and_return(mut x: i32) -> i32 {
    x = x + 1;
    return x;
}

Calling Functions

pub fn example() -> i32 {
    let result: i32 = add(10, 20);
    return result;
}

Function Body

A function body is a sequence of statements enclosed in curly braces {}.

Methods

Methods are functions defined inside an impl block. Instance methods take self as the first parameter:

struct Counter {
    value: i32;
}

impl Counter {
    fn new() -> Counter {
        return Counter { value: 0 };
    }

    fn get(self) -> i32 {
        return self.value;
    }

    fn increment(mut self) {
        self.value = self.value + 1;
    }
}

Call instance methods with dot syntax and associated functions with :::

pub fn example() -> i32 {
    let mut c: Counter = Counter::new();
    c.increment();
    return c.get();
}

Comments

Programmers often use comments to explain parts of the code that might be hard to understand or that need additional context. Comments can also describe, at a high level, what a file or function is responsible for. For these purposes, Inference supports two kinds of comments: single-line comments and docstring-style comments. Both kinds of comments are ignored by the compiler and are not part of the program itself.

Here is a simple single-line comment:

// This is a single-line comment

This is treated as a comment because the line starts with the two characters //. Everything that follows // on the same line is considered a comment and is ignored by the compiler.

You can attach a comment to a line of code, for example:

42; // The universal answer

For more descriptive explanations, Inference supports docstring-style comments that can span multiple lines. These comments start with triple forward slashes ///. Each line that begins with /// is treated as part of the same docstring comment block. For example:

/// This library provides verified cryptographic functions and primitives
/// for working with zero-knowledge proofs.

Expressions and Operators

• Arithmetic operators — +, -, *, /, %, unary -
• Comparison and logical operators — ==, !=, <, >, &&, ||, !
• Bitwise operators — &, |, ^, ~, <<, >>

Arithmetic Operators

All operators work with every integer type. Parentheses control evaluation order: (a + b) * c.

Integer Overflow

Integer arithmetic wraps on overflow, matching WebAssembly semantics. For i8, 127 + 1 wraps to -128. For u8, 0 - 1 wraps to 255. No runtime error is raised.

Division by Zero

Division and remainder by zero trap at runtime. Guard against it if the divisor may be zero:

pub fn safe_divide(a: i32, b: i32) -> i32 {
    if b == 0 {
        return 0;
    }
    return a / b;
}

Comparison and Logical Operators

Comparison Operators

All return bool. Work with all integer types. Sign-aware: i32 uses signed comparison, u32 uses unsigned.

Note

Enum values support == and != only.

Logical Operators

Operate on bool values:

Example

pub fn is_in_range(x: i32, lo: i32, hi: i32) -> bool {
    return (x >= lo) && (x <= hi);
}

Bitwise Operators

All operators work with every integer type. >> is arithmetic for signed types, logical for unsigned types.

Example

pub fn get_bit(x: i32, pos: i32) -> i32 {
    return (x >> pos) & 1;
}

pub fn set_bit(x: i32, pos: i32) -> i32 {
    return x | (1 << pos);
}

pub fn clear_bit(x: i32, pos: i32) -> i32 {
    return x & ~(1 << pos);
}

pub fn is_power_of_two(n: i32) -> bool {
    if n <= 0 {
        return false;
    }
    return (n & (n - 1)) == 0;
}

Control Flow

• Conditional statements — if and else
• Loops — loop and break

Conditional Statements

if / else

pub fn max(a: i32, b: i32) -> i32 {
    if a > b {
        return a;
    } else {
        return b;
    }
}

if / else if / else

pub fn classify(x: i32) -> i32 {
    if x > 0 {
        return 1;
    } else if x < 0 {
        return -1;
    } else {
        return 0;
    }
}

Important Differences

if is a statement, not an expression. You cannot write let x: i32 = if condition { 1 } else { 2 };. Use a mutable variable instead:

pub fn example(condition: bool) -> i32 {
    let mut result: i32 = 0;
    if condition {
        result = 1;
    } else {
        result = 2;
    }
    return result;
}

The condition must be bool. Inference does not coerce integers to booleans. Write if x != 0 { ... } instead of if x { ... }.

Curly braces are required, even for single-statement branches.

Loops

Inference uses loop for both conditional and infinite loops. There is no while or for.

Conditional Loop

pub fn sum_to_n(n: i32) -> i32 {
    let mut sum: i32 = 0;
    let mut i: i32 = 1;
    loop i <= n {
        sum = sum + i;
        i = i + 1;
    }
    return sum;
}

loop condition { body } checks the condition before each iteration. If false initially, the body never runs.

Infinite Loop

pub fn find_first_multiple(n: i32, target: i32) -> i32 {
    let mut x: i32 = n;
    loop {
        if x % target == 0 {
            break;
        }
        x = x + 1;
    }
    return x;
}

loop { body } runs until break or return.

break

break exits the innermost enclosing loop. continue is not yet supported.

Nested Loops

pub fn nested_count() -> i32 {
    let mut total: i32 = 0;
    let mut i: i32 = 0;
    loop i < 3 {
        let mut j: i32 = 0;
        loop j < 4 {
            total = total + 1;
            j = j + 1;
        }
        i = i + 1;
    }
    return total;
}

Arrays

Fixed-size, compile-time-known arrays. Sizes cannot change at runtime.

• Array basics — declaration, indexing, modification
• Arrays and functions — value semantics, returning arrays

Array Basics

Declaration

Array type is [T; N], where T is the element type and N is a compile-time constant. Supported element types: all integers, bool, struct types, and arrays (for multidimensional arrays). Every element must be provided at initialization.

let numbers: [i32; 3] = [10, 20, 30];
let flags: [bool; 4] = [true, false, true, false];
let bytes: [u8; 2] = [255, 0];

Reading and Writing Elements

pub fn modify_array() -> i32 {
    let mut data: [i32; 3] = [1, 2, 3];
    let first: i32 = data[0];     // read
    data[0] = 99;                  // write (requires mut)
    data[2] = data[0] + data[1];
    return data[2];                // returns 101
}

The index can be any integer expression, not just a literal.

Warning

Inference does not perform array bounds checking at compile time or runtime. Accessing an element beyond the array’s size results in undefined behavior.

Arrays and Functions

Value Semantics

Arrays are passed by copy. The function receives its own copy — the caller’s array is not affected:

fn modify_copy(mut arr: [i32; 3]) -> i32 {
    arr[0] = 99;
    return arr[0];
}

pub fn original_unchanged() -> i32 {
    let data: [i32; 3] = [1, 2, 3];
    let ignored: i32 = modify_copy(data);
    return data[0];  // returns 1, not 99
}

Here, mut attributes the function parameter so that arr can be modified within the function. However, this does not affect the caller’s data array, which remains unchanged.

Returning Arrays

Functions can return fixed-size arrays:

pub fn make_sequence() -> [i32; 3] {
    return [10, 20, 30];
}

pub fn use_sequence() -> i32 {
    let arr: [i32; 3] = make_sequence();
    return arr[1];
}

Array return values must be assigned to a variable first — make_sequence()[0] is not supported.

Enums

An enum defines a type with a fixed set of named variants.

Defining an Enum

enum Direction {
    North,
    South,
    East,
    West
}

pub enum exports the type from the module. Variants are comma-separated. Each enum is a distinct type.

Using Enum Values

Variants are accessed with :::

pub fn go_west() -> Direction {
    let d: Direction = Direction::West;
    return d;
}

Comparing Enums

Enums support == and !=. Ordering operators (<, >, <=, >=) are not supported.

enum Status { Active, Inactive }

pub fn is_active(s: Status) -> bool {
    return s == Status::Active;
}

pub fn are_not_equal(a: Status, b: Status) -> bool {
    return a != b;
}

Enums and Functions

Enums work as function parameters and return types like any other type:

enum Dir { Up, Down, Left, Right }

pub fn dir_to_int(d: Dir) -> i32 {
    if d == Dir::Up {
        return 10;
    }
    if d == Dir::Down {
        return 20;
    }
    if d == Dir::Left {
        return 30;
    }
    return 40;
}

Reassignment

Enum variables declared with let mut can be reassigned:

enum Color { Red, Green, Blue }

pub fn reassign() -> Color {
    let mut c: Color = Color::Red;
    c = Color::Blue;
    return c;
}

Enums in Arrays

enum Color { Red, Green, Blue }

pub fn second_color() -> i32 {
    let colors: [Color; 3] = [Color::Red, Color::Green, Color::Blue];
    if colors[1] == Color::Green {
        return 1;
    }
    return 0;
}

Enums in Structs

Enum types can be used as struct fields:

enum Status { Active, Inactive }

struct Item {
    status: Status;
    value: i32;
}

pub fn get_status() -> i32 {
    let item: Item = Item { status: Status::Inactive, value: 42 };
    if item.status == Status::Inactive {
        return 1;
    }
    return 0;
}

Note

Enums do not support data-carrying variants, explicit discriminant values, methods, or pattern matching. They are simple named constants grouped under a type for better code organization and readability.

Appendix

The appendices provide supplementary information that supports the main content of this book.

Here are the appendices included in this book:

A - Language Reference

Keywords

Data Types

Operators

Arithmetic Operators

Note

Integer arithmetic wraps on overflow. For example, adding 1 to the maximum i32 value wraps around to the minimum i32 value.

Comparison Operators

Comparison operators evaluate to a bool value.

Note

Enum values support only == and !=. Ordering comparisons (<, <=, >, >=) require numeric types.

Logical Operators

Logical operators work on bool values and produce a bool result.

Bitwise Operators

Bitwise operators work on the binary representation of integer values.

Access Operators

B - Inference Programming Language Specification

If you want to understand the foundational principles and formal definitions of the Inference programming language — including its mathematical models, syntax, and semantics — we recommend referring to the official Language Specification.

C - Inference Compiler

infc is the official compiler for the Inference programming language. It takes .inf source files and produces WebAssembly modules directly, with no external toolchain needed.

infs is the unified CLI that wraps infc with project management, toolchain installation, and build/run commands. See Appendix D for the full infs reference.

Both tools are open source and available in the inference GitHub repository. Refer there for the latest releases, discussions, and feature or bug tracking.

D - infs CLI Reference

infs is the unified command-line interface for the Inference compiler toolchain. It wraps the infc compiler with project management, toolchain installation, and build/run commands.

Compilation Commands

Build Options

infs build always runs the full compilation pipeline (parse, analyze, codegen) and writes out/<name>.wasm.

Run Options

Examples

# Full compilation (writes out/example.wasm)
$ infs build example.inf

# Compile with Rocq translation (writes out/example.wasm and out/example.v)
$ infs build example.inf -v

# Build and run
$ infs run example.inf

# Run a specific exported function
$ infs run example.inf --entry-point my_function

Using infc Directly

The underlying infc compiler accepts additional flags for selective phase execution:

When no flags are given, infc performs full compilation and writes the WASM binary — equivalent to --codegen -o.

Project Management

Creating a New Project

$ infs new myproject

This creates the following project structure:

myproject/
├── Inference.toml
├── src/
│   └── main.inf
├── tests/
└── proofs/

The generated src/main.inf contains a minimal program:

// Entry point for the Inference program

pub fn main() -> i32 {
    return 0;
}

Use --no-git to skip git initialization:

$ infs new myproject --no-git

Initializing an Existing Directory

$ infs init

Creates Inference.toml and src/main.inf in the current directory. If a .git directory exists, it also creates .gitignore and .gitkeep files.

Toolchain Management

Installing a Toolchain

# Install latest stable version
$ infs install

# Install a specific version
$ infs install 0.1.0

On first install, infs automatically configures your system PATH:

• Linux/macOS: Adds ~/.inference/bin to your shell profile (~/.bashrc, ~/.zshrc, or ~/.config/fish/config.fish)
• Windows: Updates the user PATH in the registry

After installation, restart your terminal or source your shell profile.

Checking Installation Health

$ infs doctor

This runs diagnostic checks and provides recommendations if anything needs attention.

Other Commands

Compiler Resolution

When running build or run, infs locates the infc compiler using the following priority:

Environment Variables