Clarify Inference as a dual-purpose language

README.md

@@ -5,12 +5,12 @@
 > [!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](https://inferara.com) to enable Web3 developers to formulate properties of the native application algorithms in a familiar format similar to how unit tests are written.
+Inference is a programming language that defines a high-assurance, deterministic computing model with non-deterministic extensions designed by [Inferara](https://inferara.com) for developing verifiable programs. It enables developers to write both executable code and formal specifications in a unified language, using a familiar syntax similar to imperative programming languages.
 
-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.
+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. The compiler (`infc`) targets multiple backends: generating executable binaries (currently WASM via LLVM IR) for deployment and proof units (Rocq) for formal verification.
 
 > [!IMPORTANT]
-> Inference is a Web3 native applications-oriented, formal specification language.
+> Inference is designed for both high-assurance application development and formal specification. While Web3 applications are a primary use case, the language's safety guarantees (determinism, no floating-point, static typing) make it suitable for any critical system requiring formal verification.
 
 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.
 
@@ -74,7 +74,7 @@ This repository contains the specification of the Inference programming language
     - [§4.10.3](./lexical-structure.md#4103-square-brackets) Square Brackets
       - [§4.10.3.1](./lexical-structure.md#41031-description) Description
       - [§4.10.3.2](./lexical-structure.md#41032-examples) Examples
-    - [§4.10.4](./lexical-structure.md#4104-angle-brackets) Angle Brackets
+    - [§4.10.4](./lexical-structure.md#4104-prime-symbol) Prime Symbol
       - [§4.10.4.1](./lexical-structure.md#41041-description) Description
       - [§4.10.4.2](./lexical-structure.md#41042-examples) Examples
 - [§5](./basic-concepts.md) Basic concepts
@@ -83,7 +83,7 @@ This repository contains the specification of the Inference programming language
   - [§5.3](./basic-concepts.md#53-execution-model) Execution Model
   - [§5.4](./basic-concepts.md#54-non-deterministic-execution) Non-deterministic Execution
   - [§5.5](./basic-concepts.md#55-platform-specific-execution) Platform-specific Execution
-  - [§5.6](./basic-concepts.md#56-poly-blockchain-design) Poly-blockchain Design
+  - [§5.6](./basic-concepts.md#56-platform-agnostic-design) Platform Agnostic Design
   - [§5.7](./basic-concepts.md#57-automated-reasoning) Automated Reasoning
   - [§5.8](./basic-concepts.md#58-correctness-certificate) Correctness Certificate
 - [§6](./types.md) Types
@@ -207,9 +207,10 @@ This repository contains the specification of the Inference programming language
 - [§11](./functions.md) Functions
   - [§11.1](./functions.md#111-function-definition) Function Definition
     - [§11.1.1](./functions.md#1111-description) Description
-    - [§11.1.2](./functions.md#1112-modifiers) Modifiers
-        - [§11.1.2.1](./functions.md#11121-forall) `forall`
-    - [§11.1.3](./functions.md#1113-examples) Examples
+    - [§11.1.2](./functions.md#1112-declaring-a-function) Declaring a function
+        - [§11.1.3](./functions.md#1113-modifiers) Modifiers
+            - [§11.1.3.1](./functions.md#11131-forall) `forall`
+    - [§11.1.4](./functions.md#1114-examples) Examples
   - [§11.2](./functions.md#112-external-function) External Function
     - [§11.2.1](./functions.md#1121-description) Description
     - [§11.2.2](./functions.md#1122-examples) Examples

basic-concepts.md

@@ -55,13 +55,18 @@ In this example, `sum_spec` is a `forall`-marked function that, using the `@` (u
 
 ## 5.3 Execution Model
 
-A `spec` is not an execution unit because it is mechanically impossible to execute a non-deterministic program (`@` introduces non-determinism in terms of cosidering all possibilities). The target platform of `infc` is a theorem prover. The [Inferara execution theory](TODO) enables reasoning about the program *as if it has been executed* on a certain platform. As of now, the execution platform covered by the Inferara theory is [WASM](https://webassembly.org/).
+## 5.3 Execution Model
+
+Inference serves two purposes: formal specification and high-assurance application execution.
+
+1.  **Specification**: A `spec` or any code involving non-deterministic constructs (like `@`, `forall`, `exists`, `assume`, `unique`) is not an execution unit in the traditional sense because it is mechanically impossible to execute a non-deterministic program. For these parts, the target platform is a theorem prover (Rocq), and the [Inferara execution theory](./terms-and-definitions.md#24-theory) enables reasoning about the program *as if it has been executed*.
+2.  **Execution**: "Vanilla" Inference code (structs, functions without non-determinism) is compiled to executable binaries. This code is what runs in the target environment.
 
 Essentially, the theory describes how a virtual machine (VM) works, its memory state and operations. It contains a description of how operations are executed, how memory is managed, how the stack is used, and so on. It is worth highlighting that the proof theory is not similar to symbolic execution. The symbolic execution technique actually executes commands and works with the memory state, while the proof theory is a way to describe what happens with memory after a command is executed without having this memory in the real world.
 
 For illustration, consider the well-known formula of energy $E=mc^2$. This formula is a property of one aspect of how the universe works. In order to prove this formula, other formulas and theories are used. However, the formula itself is not proven by experiment simply because an experiment cannot cover all possible combinations of $m$ and $c$ to ensure the formula is correct for all possible values.
 
-In this analogy, the Inference proof is akin to a mathematical proof, whereas symbolic execution is akin to an experimental approach.
+In this analogy, the Inference proof is akin to a mathematical proof, whereas symbolic execution (and actual execution) is akin to an experimental approach. Inference allows you to write the application and the "mathematical proof" (spec) in the same language.
 
 ## 5.4 Non-Deterministic Execution
 
@@ -101,11 +106,17 @@ So when Inference reasons about a DApp, it reasons about the DApp itself, and th
 
 However, it does not limit Inference usage for DApps only. Inference can be used to reason about any program that is a part or a blockchain itself. For example, a consensus algorithm can be extracted from the setting where host functions are used and a `spec` can be created to describe its behavior.
 
-## 5.6 Poly-Blockchain Design
+## 5.6 Platform Agnostic Design
+
+Inference is a low-level language because property definitions must be straightforward and unambiguous. From the [proof-unit](./terms-and-definitions.md#25-proof-unit) viewpoint, the execution model follows the command set of a certain platform—for example, WASM.
+
+However, the language design itself is **platform agnostic**. The `infc` compiler is modular, meaning:
 
-Inference is a low-level language because property definitions must be straightforward and unambiguous. From the [proof-unit](./terms-and-definitions.md#25-proof-unit) viewpoint, the execution model follows the command set of a certain platform—for example, WASM. This means that if a blockchain uses WASM as a compilation target (or can be compiled to with the unchanged semantic), then compiled DApp modules can be linked to the Inference modules, and proofs can be constructed.
+1.  **Frontend**: The Inference language remains the same regardless of the target.
+2.  **Backend**: `infc` generates IR for a specific target (currently WASM).
+3.  **Verification**: The Inferara theory corresponds to the target platform's execution model.
 
-For reference, the following blockchains use WASM as a compilation target:
+Currently, WASM is the fully supported target because many blockchains use WASM as a compilation target:
 
 - [Stellar](https://www.stellar.org/)
 - [Polkadot](https://polkadot.network/)
@@ -143,7 +154,7 @@ Since the final artifact of `infc` is a Rocq file `.v`, it can be checked by the
 
 Furthermore, correctness tracking is also available, so we can check if the proof for the code at state $S$ is equivalent to the proof for the code at state $S'$.
 
-There is a [database](#TODO) of correctness certificates that Inferara holds, and it is possible to ensure if a given code has been proven before and if the proof is still valid.
+There is a database of correctness certificates that Inferara holds, and it is possible to ensure if a given code has been proven before and if the proof is still valid.
 
 ---
 

general-description.md

@@ -4,8 +4,8 @@ Inference is a formal specification language that aims to provide a straightforw
 
 > [!IMPORTANT]
 > Based on this fact, the following important consequences follow:
-> 1. Inference is a Turing-complete language, **but**
-> 2. It is not intended to be used for general-purpose programming.
+> 1. Inference is a Turing-complete language.
+> 2. It is designed to be used for both formal specification and high-assurance application development.
 
 ## 3.1 Non-Deterministic Computations
 
@@ -202,12 +202,22 @@ The compilation process consists of the following stages:
 1. Inference source code parsing using [tree-sitter-inference](https://github.com/Inferara/tree-sitter-inference) grammar parser.
    - Building required internal representations.
    - Semantic analysis and type checking. [Tracking issue](https://github.com/Inferara/inference/issues/8)
-   - Linked external modules integrity and capability check.
-2. Generating IR for the target execution platform (WASM) amended with Inference non-deterministic instructions.
-3. Building a compound module containing the Inference module IR and linked external code.
-4. Translating the compound module to a [proof-unit](./terms-and-definitions.md#25-proof-unit).
-5. Attaching Inference [theory](./terms-and-definitions.md#24-theory), platform axioms, and generating theorems.
-6. Building proofs for the specification.
+2. Linked external modules integrity and capability check.
+3. For **Formal Specification**:
+   - Generating `ll` with `inf intrinsics` (Inference non-deterministic instructions).
+   - Lowering `ll` to the target architecture (currently primarily WASM) using `inf-llc`.
+   - Translating the compound module to a [proof-unit](./terms-and-definitions.md#25-proof-unit).
+   - Attaching Inference [theory](./terms-and-definitions.md#24-theory), platform axioms.
+   - Inferencing theorems.
+   - Building proofs for the specification.
+4. For **Application Execution**:
+   - "Vanilla" structs and modules (executable code) are lowered to LLVM IR (`ll`).
+   - The LLVM IR is compiled to the target architecture (currently primarily WASM) using `inf-llc` with appropriate flags that force high level of optimization.
+
+This workflow enables using Inference for both safe application development and formal specification at the same time. In the same file or project, developers can write the executable code and its formal specification. The formal verification prover uses the exact code written as an application to verify it, and then the compiled module can be deployed to the target environment.
+
+> [!NOTE]
+> While WASM is the current primary target for both execution and verification mechanization, the `infc` architecture is modular. Support for other architectures (like RISC-V or EVM) can be added by extending the compiler backend and the corresponding verification theory.
 
 ![Inference IR Building Sequence](./assets/inference-ir-building-sequence.png)
 

introduction.md

@@ -32,10 +32,10 @@ Inference is designed with the computer-assisted theorem proving technique in mi
 
 Speaking about Inference as a special-purpose programming language, it is important to list significant considerations that were taken into account during the language design:
 
-- Inference is intended to be a simple, concise, unambiguous, and easy-to-understand formal specification language.
+- Inference is intended to be a simple, concise, unambiguous, and easy-to-understand language for both formal specification and high-assurance application development.
 - The language should have the feel of an imperative language and hide all the complexity of formal verification details.
-- The language is intended for use in developing Web3 applications as a correctness specification language that ensures the application's properties and certifies the application's correctness.
-- The language evolves in the direction of improving the power of automated deduction and being applicable to a wide range of blockchain architectures.
+- The language is intended for use in developing critical systems as a dual-purpose language: writing efficient, safe executables and their correctness specifications in the same codebase.
+- The language evolves in the direction of improving the power of automated deduction and being applicable to a wide range of architectures (e.g., WASM, RISC-V, EVM).
 - Support for modern IDEs and code editors is very important.
 
 ---

terms-and-definitions.md

@@ -6,7 +6,7 @@ Decentralized Applications (DApps) are applications that run on a decentralized
 
 ## 2.2 `infc`
 
-Inference Compiler (`infc`) is a tool that compiles Inference programs into proof code. The compiler is responsible for parsing the Inference code, type-checking it, and generating the output code. The source code is located in the [Inference](https://github.com/Inferara/inference) repository.
+Inference Compiler (`infc`) is a tool that compiles Inference programs into proof code and executable binaries. The compiler is responsible for parsing the Inference code, type-checking it, generating the output code (LLVM IR -> Target Binary for execution, Rocq for verification). The source code is located in the [Inference](https://github.com/Inferara/inference) repository.
 
 ## 2.3 Module