EML-lang in 30 Minutes

1. Write your first equation in EML-lang
2. Compile it to 22 targets (C, Rust, Verilog, Lean, …)
3. Read a chain-order profile
4. Build a PID controller
5. Add formal verification
6. Target an FPGA
7. Compile your own equation to silicon

No programming experience required. EML-lang is math with curly braces.

Your first equation

The simplest possible program

Create a file called hello.eml:

hello.emlfn add(a: Real, b: Real) -> Real {
    a + b
}

That's it. You just wrote EML-lang.

Let's break it down:

fn              → "I'm defining a function"
add             → the name (you pick this)
(a: Real,       → first input, it's a real number
 b: Real)       → second input, also a real number
-> Real         → this function returns a real number
{               → start of the math
    a + b       → the equation (just addition)
}               → end

Compile it

bashpython tools/cli/main.py hello.eml --target all -o ./my_first

What you get

my_first/
  hello.c           ← your equation in C
  hello.cpp         ← your equation in C++
  hello.rs          ← your equation in Rust
  hello.py          ← your equation in Python
  hello.ll          ← your equation in LLVM IR
  hello.wasm.ll     ← your equation in WebAssembly
  hello.lean        ← your equation as a Lean theorem
  hello.v           ← your equation in Verilog (hardware!)
  hello.sv          ← your equation in SystemVerilog
  hello.vhd         ← your equation in VHDL
  Hello.scala       ← your equation in Chisel
  hello.ads         ← your equation in Ada/SPARK (spec)
  hello.adb         ← your equation in Ada/SPARK (body)
  hello.m           ← your equation in MATLAB
  hello.go          ← your equation in Go
  hello.kt          ← your equation in Kotlin
  Hello.java        ← your equation in Java
  hello.aadl        ← your equation as an AADL component
  hello.arxml       ← your equation as an AUTOSAR SWC
  hello_pkg/        ← your equation as a ROS2 package

Open hello.c and look:

hello.c// Generated by Monogate Forge
// Source: hello.eml
// Chain order: 0 | Cost class: p0-d2-w0-c0

double add(double a, double b) {
    return a + b;
}

Your equation. In C. Ready to compile and run.

Open hello.v and look:

hello.v// Generated by Monogate Forge
// Source: hello.eml
// Chain order: 0 | FPGA: 1 MAC unit

module add (
    input  wire signed [63:0] a,
    input  wire signed [63:0] b,
    output wire signed [63:0] result
);
    assign result = a + b;
endmodule

Your equation. In hardware. Ready for an FPGA.

You just compiled math to silicon. In one command.

Constants and real math

Adding constants

gravity.emlconst g: Real = 9.81
const half: Real = 0.5

fn fall_distance(t: Real) -> Real {
    half * g * t * t
}

fn fall_velocity(t: Real) -> Real {
    g * t
}

const gives a name to a number. Same as any language.

Using transcendental functions

These are the functions that make EML-lang special:

transcendental.emlfn exponential_decay(t: Real, k: Real) -> Real {
    exp(-k * t)
}

fn oscillation(t: Real, freq: Real) -> Real {
    sin(freq * t)
}

fn damped_wave(t: Real, decay: Real, freq: Real) -> Real {
    exp(-decay * t) * cos(freq * t)
}

The available math functions:

FUNCTION       WHAT IT DOES                 CHAIN ORDER
─────────────────────────────────────────────────────────
+ - * /        arithmetic                   0
exp(x)         e to the x                   adds 1
ln(x)          natural log of x             adds 1
sin(x)         sine                         adds 2
cos(x)         cosine                       adds 2
tan(x)         tangent                      adds 2
sqrt(x)        square root                  0
tanh(x)        hyperbolic tangent           adds 2
arcsin(x)      inverse sine                 adds 2
arccos(x)      inverse cosine               adds 2
atan2(y, x)    angle from coordinates       adds 2
abs(x)         absolute value               0
clamp(x, l, h) clip to range                0
min(a, b)      smaller of two               0
max(a, b)      larger of two                0
pow(x, y)      x to the y                   0 to 1
eml(x, y)      exp(x) - ln(y)               adds 1

Compile and read the profile

bashpython tools/cli/main.py transcendental.eml --explain

The compiler tells you about each function:

exponential_decay:
  chain_order: 1            ← one transcendental layer (exp)
  cost_class:  p1-d3-w1-c0
  drift_risk:  LOW          ← safe at float32

damped_wave:
  chain_order: 3            ← three layers (exp + cos)
  cost_class:  p3-d5-w2-c1
  drift_risk:  MEDIUM       ← use float64 for precision

What chain order means (plain English)

Chain 0:   Just arithmetic. x + y, x * y, x^2.
           Simple. Fast. Always precise.
           Safe at any precision (even float16).

Chain 1:   One exp or ln involved.
           Like exponential decay, compound interest.
           Still safe. Slight precision consideration.

Chain 2:   Trig involved. sin, cos, tanh.
           Like oscillations, waves, rotations.
           Needs float32 minimum.

Chain 3+:  Multiple layers nested.
           Like exp(sin(x)) or damped oscillators.
           Needs float64. FPGA needs more hardware units.
           The compiler warns you automatically.

PID controller

The most common equation in all of engineering

Every robot, drone, car, thermostat, and factory uses PID:

pid_controller.emlconst Kp: Real = 2.5      // proportional gain
const Ki: Real = 0.1      // integral gain
const Kd: Real = 0.05     // derivative gain

fn pid(error: Real, integral: Real, derivative: Real) -> Real {
    Kp * error + Ki * integral + Kd * derivative
}

That's a complete PID controller.

Compile it

bashpython tools/cli/main.py pid_controller.eml --target all -o ./pid_out

What the compiler tells you

pid:
  chain_order: 0              ← purely polynomial (no exp/sin)
  nodes:       6              ← 6 arithmetic operations
  cost_class:  p0-d6-w0-c0
  drift_risk:  NONE           ← safe at ANY precision
  fpga_estimate:
    exp_units: 0              ← no transcendental hardware
    luts:      ~50            ← tiny FPGA footprint
    latency:   3 cycles       ← 30 ns at 100 MHz

Chain order 0 means this PID is just arithmetic. No exp. No sin. Pure math. Runs on the smallest FPGA chip you can buy. 30 nanoseconds per cycle.

Now make it nonlinear

nonlinear_pid.emlconst Kp: Real = 2.5
const decay: Real = 0.1
const freq: Real = 10.0

fn adaptive_pid(error: Real, t: Real) -> Real {
    let gain = exp(-decay * t) * cos(freq * t);
    gain * Kp * error
}

Compile it again. Now the compiler says:

adaptive_pid:
  chain_order: 3              ← jumped from 0 to 3!
  drift_risk:  MEDIUM         ← float64 recommended
  fpga_estimate:
    exp_units:  1             ← needs exp hardware
    trig_units: 1             ← needs cos hardware
    luts:       ~300          ← 6× more FPGA resources

The compiler told you the complexity jumped. Before you ran anything. Before you built any hardware. Before you spent any money. The chain order predicts the cost.

Formal verification

Making the compiler PROVE your math is correct

Add @verify to any function:

safe_pid.emlconst Kp: Real = 2.5
const Ki: Real = 0.1
const max_output: Real = 100.0

@verify(lean, theorem = "pid_is_bounded")
fn safe_pid(error: Real, integral: Real) -> Real
    requires (abs(error) < 50.0)
    requires (abs(integral) < 500.0)
    ensures  (abs(result) < max_output)
{
    Kp * error + Ki * integral
}

What the new keywords mean:

@verify(lean, theorem = "pid_is_bounded")
  → "Generate a Lean proof for this function"
  → The theorem will be named "pid_is_bounded"

requires (abs(error) < 50.0)
  → "This function only works when error is between -50 and 50"
  → If someone passes error = 999, that's THEIR bug, not yours

ensures (abs(result) < max_output)
  → "I PROMISE the output is always between -100 and 100"
  → The compiler generates a PROOF of this promise

Compile with verification

bashpython tools/cli/main.py safe_pid.eml --target lean -o ./verified.lean

Open verified.lean:

leanimport MachLib.EML
import MachLib.Trig

open MachLib
open MachLib.Real

def safe_pid (error integral : Real) : Real :=
  2.5 * error + 0.1 * integral

theorem pid_is_bounded
    (error integral : Real)
    (h1 : abs error < 50.0)
    (h2 : abs integral < 500.0) :
    abs (safe_pid error integral) < 100.0 := by
  unfold safe_pid
  sorry  -- TODO: prove against MachLib foundations

The compiler generated the theorem statement. The sorry means the proof isn't filled in yet. That's where MachLib's proof corpus (or an agent) closes it.

Why this matters

WITHOUT @verify:
  "I think my PID output stays under 100."
  "It worked in testing."
  "Ship it and hope."

WITH @verify:
  "The Lean theorem prover proved my PID output stays
   under 100 for all valid inputs."
  "Here's the proof certificate."
  "The math is guaranteed, not hoped."

One annotation, many provers

The same @verify(lean, ...) block also drives Coq, Isabelle/HOL, Ada SPARK Pre/Post aspects, SystemVerilog SVA assertions, MATLAB asserts, Java/Kotlin/Go runtime guards, and Doxygen contract comments. One source. Twelve target ecosystems hit by one annotation.

bashpython tools/cli/main.py safe_pid.eml --target coq      -o ./safe.v
python tools/cli/main.py safe_pid.eml --target isabelle -o ./Safe.thy
python tools/cli/main.py safe_pid.eml --target ada      -o ./safe.adb

Hardware target

Putting your math on a chip

Add @target(fpga) to any function:

fpga_pid.emlconst Kp: Real = 2.5
const Ki: Real = 0.1

@target(fpga, clock_mhz = 100)
fn hardware_pid(error: Real, integral: Real) -> Real {
    Kp * error + Ki * integral
}

Compile to Verilog (or SystemVerilog)

bashpython tools/cli/main.py fpga_pid.eml --target verilog -o ./hw/pid.v
python tools/cli/main.py fpga_pid.eml --target systemverilog -o ./hw/pid.sv

The compiler tells you:

hardware_pid:
  FPGA allocation:
    target:    Xilinx Artix-7
    LUTs:      48
    DSP blocks: 2
    exp units: 0 (not needed — chain 0)
    clock:     100 MHz
    latency:   2 cycles (20 ns)
    utilization: 0.07% of Artix-7 budget

Open hw/pid.v:

verilog// Generated by EML-lang Verilog backend
// Chain order: 0 | 48 LUTs | 2 DSPs | 20 ns latency

module hardware_pid_pipeline #(
    parameter WIDTH = 32
) (
    input  wire             clk,
    input  wire             rst,
    input  wire             valid_in,
    input  wire signed [WIDTH-1:0] error,
    input  wire signed [WIDTH-1:0] integral,
    output reg              valid_out,
    output reg signed [WIDTH-1:0] result
);
    wire signed [WIDTH-1:0] _w1, _w2, _w3;
    assign _w1 = Kp * error;
    assign _w2 = Ki * integral;
    assign _w3 = _w1 + _w2;

    always @(posedge clk) begin
        if (rst) begin
            valid_out <= 1'b0;
            result    <= '0;
        end else begin
            valid_out <= valid_in;
            result    <= _w3;
        end
    end
endmodule

That's your equation. As a hardware module. Ready to load onto a $50 FPGA board.

What the numbers mean

LUTs:      Logic blocks on the FPGA. 48 out of 63,400 available.
           Your PID uses 0.07% of the chip. Basically free.

DSPs:      Dedicated multiplier blocks. 2 out of 240 available.
           One for each multiplication (Kp*error, Ki*integral).

Latency:   How many clock cycles to compute one result.
           2 cycles at 100 MHz = 20 nanoseconds.
           That's 50,000,000 PID computations per second.

For comparison:
  PLC:     1 PID computation per millisecond (1,000/sec)
  FPGA:    50,000,000 PID computations per second

  50,000× faster. On a chip that costs $50 instead of $5,000.

Your own project

Pick any equation you know

Here are ideas based on what you do:

IF YOU'RE A MECHANICAL ENGINEER:
  Spring-mass-damper: F = -k*x - c*v
  Heat transfer:      Q = h*A*(T_surface - T_fluid)
  Stress:             sigma = F / A

IF YOU'RE AN ELECTRICAL ENGINEER:
  RC decay:       V = V0 * exp(-t / (R*C))
  RLC oscillator: V = V0 * exp(-R*t/(2*L)) * cos(omega*t)
  Ohm's law:      V = I * R

IF YOU'RE A CHEMICAL ENGINEER:
  Arrhenius:       k = A * exp(-Ea / (R*T))
  First-order:     C = C0 * exp(-k*t)
  pH:              pH = -ln(H_concentration) / ln(10)

IF YOU'RE A GAME DEVELOPER:
  Projectile:      y = v0*t - 0.5*g*t*t
  Bounce decay:    y = A * exp(-d*t) * abs(sin(omega*t))
  Camera smoothing: pos = lerp(curr, target, 1 - exp(-speed*dt))

IF YOU DON'T KNOW WHAT EQUATION TO USE:
  Just do this:

  fn my_function(x: Real) -> Real {
      exp(x) * sin(x)
  }

  Compile it. See what happens.

Write it

my_project.emlconst k: Real = 100.0     // spring constant
const c: Real = 5.0       // damping coefficient
const m: Real = 1.0       // mass

fn spring_force(x: Real, v: Real) -> Real {
    (-k * x - c * v) / m
}

@verify(lean, theorem = "force_proportional")
fn verified_spring(x: Real, v: Real) -> Real
    requires (abs(x) < 10.0)
    requires (abs(v) < 100.0)
    ensures  (abs(result) < 1500.0)
{
    spring_force(x, v)
}

@target(fpga, clock_mhz = 200)
fn realtime_spring(x: Real, v: Real) -> Real {
    spring_force(x, v)
}

Compile everything

bashpython tools/cli/main.py my_project.eml --target all -o ./my_build

What you just did

In 30 minutes you:

  1. Learned EML-lang syntax (fn, const, Real)
  2. Used transcendental functions (exp, sin, cos)
  3. Read chain-order profiles
  4. Built a PID controller
  5. Added formal verification (@verify)
  6. Targeted FPGA hardware (@target)
  7. Compiled YOUR OWN equation to 22 targets

You can now:
  - Write any equation in EML-lang
  - Compile it to C, C++, Rust, Verilog, SystemVerilog,
    Lean, Coq, Isabelle, Ada/SPARK, MATLAB, ROS2,
    Java, Kotlin, Go, AUTOSAR, AADL, Solidity, and 5 more
  - Read the structural profile (chain order, drift risk)
  - Add formal proofs to safety-critical functions
  - Deploy to FPGA hardware

One equation. Twenty-two targets. Verified. Write math. Get silicon — and smart contracts.

Print this and pin it to your wall.

SYNTAX
  const NAME: Real = VALUE
  fn NAME(x: Real, y: Real) -> Real { equation }
  let temp = sub_expression;
  if condition { a } else { b }

MATH
  +  -  *  /                  arithmetic
  exp(x)  ln(x)               exponential / log
  sin(x)  cos(x)  tanh(x)     trigonometric
  sqrt(x)  abs(x)             utilities
  min(a, b)  max(a, b)        comparison
  clamp(x, lo, hi)            saturating clip
  arcsin(x)  arccos(x)        inverse trig
  atan2(y, x)                 angle from (x, y)
  pow(x, y)                   x to the y
  eml(x, y) = exp(x) - ln(y)  fundamental EML operator

ANNOTATIONS
  @verify(lean, theorem = "name")  generate a formal proof
  @target(fpga, clock_mhz = N)     compile to FPGA
  requires CONDITION               input precondition
  ensures  CONDITION               output postcondition

COMPILE
  python tools/cli/main.py file.eml --target all -o ./out
  python tools/cli/main.py file.eml --target c -o out.c
  python tools/cli/main.py file.eml --target verilog -o out.v
  python tools/cli/main.py file.eml --target lean -o out.lean

PROFILE READING
  chain_order: 0   polynomial (simple, always safe)
  chain_order: 1   exponential (one layer, safe)
  chain_order: 2   trigonometric (needs float32+)
  chain_order: 3+  nested (needs float64, more FPGA)
  drift_risk: LOW / MEDIUM / HIGH  precision warning

You finished. Now what?

1. Browse the examples. monogate-forge/industries/ — 18 verticals with real .eml files you can study.
2. Read the language guide. monogate-forge/docs/language_guide.md.
3. Try the interactive demos. 1op.io/playground.
4. Join the ecosystem.
   • monogateforge.com → the compiler
   • machlib.org → machine-native math library
   • capcard.ai → agent certification
   • monogate.org → the research behind it all