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.

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 and Windows
• Writing a program that returns a mysterious number 42

Installation

To install Inference you need to download binary files 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 $.

Installing Inference on Linux and macOS

Installation on Linux is as simple as downloading the release artifact, extracting it, and adding an executable infc to your system PATH.

Note

infcis compiled for apple silicon cpu architecture, so if you are using an Intel-based mac, you may need to run it under Rosetta 2 or build from source.

Installing Inference on Windows

For Windows, some additional libraries are required to run infc. If you already have some other LLVM-based tools installed, you may already have the required dependencies. Otherwise, there is a PowerShell script included in the infc package that can check for and install any missing dependencies using the MSYS2 package manager.

Verifying Downloaded Package

To verify the integrity of the downloaded package, you can check its SHA256 checksum. The checksum value is provided on the infc GitHub Releases page alongside the download links.

On Linux/macOS, run the following command in the terminal:

$ sha256sum infc-linux-x86_64.tar.gz

On Windows, run the following command in PowerShell:

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

infc is distributed with required dependencies in a compressed archive. After downloading the appropriate package for your operating system, extract its contents to a directory of your choice. And verify that you have the following files in the extracted directory:

infc-directory
├──bin
│   └── inf-llvm            (or inf-llvm.exe on Windows)
│   └── rust-lld            (or rust-lld.exe on Windows)
├──lib                      (Linux only)
│    └── libLLVM.so.*       (LLVM shared library)
├──check_deps.ps1           (Windows only)
└──infc                     (or infc.exe on Windows)

Understading the files:

• infc is the Inference compiler executable;
• inf-llvm is a custom LLVM toolchain used by the Inference compiler to generate binaries;
• rust-lld is a Rust linker used by the Inference compiler to link compiled modules into executable binaries.
• libLLVM.so.* is the LLVM shared library required by inf-llvm on Linux systems;
• check_deps.ps1 is a PowerShell script to verify that all required dependencies are installed on Windows systems.

Ensure Required Dependencies are Installed on Windows

On Windows, open PowerShell, navigate to the extracted infc directory, and run the following command to check for required dependencies:

> .\check_deps.ps1

Tip

If you encounter an execution policy error, right click the check_deps.ps1 file in file explorer, select Properties, and choosing Unblock if that option appears at the bottom of the Properties tab.

This script will verify that all necessary dependencies are installed on your system. If any dependencies are missing, the script will ask your permission to install them automatically using pacman.

Note

The script assumes you have MSYS2 installed in C:\msys64

As a final result, you should see the following output:

--- INFC Dependency Check Starting ---
Directory: D:\GitHub\infc
[FOUND]    libwinpthread-1.dll (in PATH: C:\msys64\ucrt64\bin\libwinpthread-1.dll)
[FOUND]    libffi-8.dll (in PATH: C:\msys64\ucrt64\bin\libffi-8.dll)
[FOUND]    libgcc_s_seh-1.dll (in PATH: C:\msys64\ucrt64\bin\libgcc_s_seh-1.dll)
[FOUND]    libzstd.dll (in PATH: C:\msys64\ucrt64\bin\libzstd.dll)
[FOUND]    zlib1.dll (in PATH: C:\msys64\ucrt64\bin\zlib1.dll)
---------------------------------
SUCCESS: All identified dependencies are present.
Ready to run Inference

Add infc to your system PATH:

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

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

On Windows, run the following command in PowerShell:

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

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:

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:

• 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.

We see that the hello_world function is defined without any container or module. If Inference sees such a function in a file, a standard module is created automatically and the function is placed inside it. To be able to call this function from outside the module, the export attribute is added automatically to the function.

Compiling the Program

To compile an .inf file into an executable binary, we use the Inference compiler, which is invoked via the command line using the infc command. Open your terminal, navigate to the directory where you saved hello_world.inf, and run the following command:

On Linux or macOS:

$ infc --codegen -o hello_world.inf

On Windows:

> infc --codegen -o hello_world.inf

As a result, the compiler will generate a Wasm binary module named hello_world.wasm in the out directory.

The --codegen flag tells the compiler to generate code, and link modules. The -o flag tells the compiler to output directory.

Running the Program

To execute the compiled Wasm binary, we can use any preferred Wasm runtime. In this example and in 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 hello_world.wasm binary using the following command:

On Linux or macOS:

$ wasmtime hello_world.wasm --invoke hello_world

On Windows:

> wasmtime 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, functions, and comments. Understanding these concepts is essential for writing programs in Inference.

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

Data Types

Inference is a statically typed language, which means every value and variable must have a known type at compile time. This allows the compiler to catch type-related errors early in the development process, leading to more reliable and maintainable code.

Integer Types

An integer is a numeric type that represents whole numbers without fractional components. We already encountered the i32 integer type in the Hello World example. The leading i stands for “integer,” and the number 32 indicates how many bits are used to represent the value. The highest-order bit is used for the sign: 0 for non-negative values and 1 for negative values. Thus, the standard calculation for the range of values that can be represented by a signed integer type is from -2^(n-1) to 2^(n-1) - 1, where n is the number of bits.

Integer types are language primitives and cannot be extended or modified. Inference supports the following integer types:

Floating-Point Types

Inference does not support floating-point types. Instead, it focuses on integer and fixed-point arithmetic to ensure determinism and precision in computations. This design choice is particularly important for applications requiring high assurance and correctness.

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 have already done in the Hello World chapter, the smallest Inference program is a function.

Anatomy of a Function

In Inference, a general function blueprint looks like this:

fn function_name() -> return_type {
    ...
}

Function Body

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

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.

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

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 is open source and available in the inference GitHub repository. Refer there for the latest releases, discussions, and feature or bug tracking.