Inference programming language specification

Warning

This document is a work in progress. The content is subject to change. Some sections may be incomplete or missing. Please stay tuned for updates.

Inference is a domain-specific programming language designed by Inferara to enable Web3 developers to formulate properties of the native application algorithms in a familiar format similar to how unit tests are written.

Inference allows formal proof of the correctness of the specified properties to be expressed as a theorem-prover theory and verified in an automated way.

Important

Inference is a Web3 native applications-oriented, formal specification language.

This repository contains the specification of the Inference programming language. The specification is divided into several sections, each describing a specific aspect of the language. The language is designed to be simple and easy to learn, and its syntax is concise and similar to Rust.

Table of contents

• Foreword
• §1 Introduction
• §2 Terms and definitions
  • §2.1 DApp
  • §2.2 infc
  • §2.3 Module
  • §2.4 Theory
  • §2.5 Proof-Unit
• §3 General description
  • §3.1 Non-Deterministic Computations
    • §3.1.1 Forall
    • §3.1.2 Exists
    • §3.1.3 Assume
    • §3.1.4 Uzumaki
      • §3.1.4.1 Semantics
      • §3.1.4.2 Examples
  • §3.2 Compiler Design
  • §3.3 Automated Theorem Proving
  • §3.4 Restrictions
• §4 Lexical structure
  • §4.1 Comments
    • §4.1. Description
    • §4.1.2 Examples
  • §4.2 Keywords
  • §4.3 Identifiers
    • §4.3.1 Description
    • §4.3.2 Examples
  • §4.4 Reserved Identifiers
  • §4.5 Qualified Identifiers
    • §4.5.1 Description
    • §4.5.2 Examples
  • §4.6 Member Access
    • §4.6.1 Description
    • §4.6.2 Examples
  • §4.7 Literals
    • §4.7.1 Bool
      • §4.7.1.1 Description
      • §4.7.1.2 Examples
    • §4.7.2 Unit
      • §4.7.2.1 Description
      • §4.7.2.2 Examples
  • §4.8 Right Arrow
    • §4.8.1 Description
    • §4.8.2 Examples
  • §4.9 Terminator
    • §4.9.1 Description
    • §4.9.2 Examples
  • §4.10 Braces
    • §4.10.1 Curly Braces
      • §4.10.1.1 Description
      • §4.10.1.2 Examples
    • §4.10.2 Parentheses
      • §4.10.2.1 Description
      • §4.10.2.2 Examples
    • §4.10.3 Square Brackets
      • §4.10.3.1 Description
      • §4.10.3.2 Examples
    • §4.10.4 Angle Brackets
      • §4.10.4.1 Description
      • §4.10.4.2 Examples
• §5 Basic concepts
  • §5.1 Specification Definition
  • §5.2 Specification Is Not a Program
  • §5.3 Execution Model
  • §5.4 Non-deterministic Execution
  • §5.5 Platform-specific Execution
  • §5.6 Poly-blockchain Design
  • §5.7 Automated Reasoning
  • §5.8 Correctness Certificate
• §6 Types
  • §6.1 Unit
    • §6.1.1 Description
    • §6.1.2 Examples
  • §6.2 Elementary Types
    • §6.2.1 Boolean
      • §6.2.1.1 Description
      • §6.2.1.2 Examples
    • §6.2.2 Integers
      • §6.2.2.1 Description
      • §6.2.2.2 Examples
    • §6.2.3 Unsigned Integers
      • §6.2.3.1 Description
      • §6.2.3.2 Examples
    • §6.3 Array
      • §6.3.1 Description
      • §6.3.2 Examples
    • §6.4 Function type
      • §6.4.1 Description
      • §6.4.2 Examples
    • §6.5 User-defined Types
      • §6.5.1 Description
• §7 Variables
  • §7.1 General Description
  • §7.2 Variable Categories
    • §7.2.1 Local Variables
      • §7.2.1.1 Description
      • §7.2.1.2 Examples
    • §7.2.2 Array Elements
      • §7.2.2.1 Description
      • §7.2.2.2 Examples
  • §7.3 Default Values
    • §7.3.1 Description
    • §7.3.2 Examples
  • §7.4 Variable Definition and Assignment
    • §7.4.1 Description
    • §7.4.2 Block Statement
      • §7.4.2.1 Description
      • §7.4.2.2 Examples
    • §7.4.3 Loop Statement
      • §7.4.3.1 Description
      • §7.4.3.2 Examples
• §8 Expressions
  • §8.1 Assign
    • §8.1.1 Description
    • §8.1.2 Examples
  • §8.2 Member Access
    • §8.2.1 Description
    • §8.2.2 Examples
  • §8.3 Array Index Access
    • §8.3.1 Description
    • §8.3.2 Examples
  • §8.4 Function Call
    • §8.4.1 Description
    • §8.4.2 Examples
  • §8.5 Parenthesized
    • §8.5.1 Description
    • §8.5.2 Examples
  • §8.6 Unary Operators
    • §8.6.1 Description
    • §8.6.2 Examples
  • §8.7 Binary Operators
    • §8.7.1 Description
    • §8.7.2 Examples
• §9 Statements
  • §9.1 Block
    • §9.1.1 Description
    • §9.1.2 Examples
  • §9.2 Return
    • §9.2.1 Description
    • §9.2.2 Examples
  • §9.3 Forall
  • §9.4 Exists
  • §9.5 Assume
    • §9.5.1 Description
    • §9.5.2 Examples
  • §9.6 Unique
    • §9.6.1 Description
    • §9.6.2 Examples
  • §9.7 Loop
    • §9.7.1 Description
    • §9.7.2 Examples
  • §9.8 If
    • §9.8.1 Description
    • §9.8.2 Examples
  • §9.9 Variable Definition
    • §9.9.1 Description
    • §9.9.2 Value Modifiers
      • §9.9.2.1 Uzumaki
    • §9.9.3 Examples
  • §9.10 Type Definition
    • §9.10.1 Description
    • §9.10.2 Examples
  • §9.11 Assert
    • §9.11.1 Description
    • §9.11.2 Examples
• §10 Definitions
  • §10.1 Constant
    • §10.1.1 Description
    • §10.1.2 Examples
  • §10.2 Function
    • §10.2.1 Description
    • §10.2.2 Examples
  • §10.3 External Function
    • §10.3.1 Description
    • §10.3.2 Examples
  • §10.4 Type
    • §10.4.1 Description
    • §10.4.2 Examples
  • §10.5 Spec
    • §10.5.1 Description
    • §10.5.2 Examples
  • §10.6 Enum
    • §10.6.1 Description
    • §10.6.2 Examples
  • §10.7 Struct
    • §10.7.1 Description
    • §10.7.2 Examples
• §11 Functions
  • §11.1 Function Definition
    • §11.1.1 Description
    • §11.1.2 Modifiers
      • §11.1.2.1 forall
    • §11.1.3 Examples
  • §11.2 External Function
    • §11.2.1 Description
    • §11.2.2 Examples
  • §11.3 High-order Functions
    • §11.3.1 Description
    • §11.3.2 Examples
• §12 Constants
  • §12.1 Description
  • §12.2 Examples
• §13 Directives
  • §13.1 Use Directive
    • §13.1.1 Description
    • §13.1.2 Examples
• §A Grammar
• §B Standard Library
• §C Comments
  • C001
  • C002
• §D Examples
• §E Bibliography
  • §E.1 Inferara Papers
  • §E.2 Books
  • §E.3 Articles
  • §E.4 Links