EML-lang in 30 Minutes

1. Write your first equation in EML-lang
2. Emit selected software artifacts and inspect them
3. Read a chain-order profile
4. Build a PID controller
5. Add a proof-shaped obligation
6. Preview a hardware-target profile
7. Build a bounded project artifact

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 python,c -o ./my_first

What you get

my_first/
  hello.py          ← selected Python artifact
  hello.c           ← selected C artifact
  profile.json      ← structural profile and claim boundary

Open hello.c and look:

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

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

Your equation, lowered into a small C artifact for inspection and local validation.

The evidence shape

The point is not to pretend every target is already production-ready. The point is to keep the artifact, profile, evidence packet, and reviewer boundary close together.

You just turned one equation into selected inspectable artifacts with an explicit evidence boundary.

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          ← check the sample range

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.
           Usually simplest. Low drift risk on normal ranges.
           Still validate your numeric range.

Chain 1:   One exp or ln involved.
           Like exponential decay, compound interest.
           Often manageable. Check domains and exponent size.

Chain 2:   Trig involved. sin, cos, tanh.
           Like oscillations, waves, rotations.
           Usually wants float32+ and sample-grid checks.

Chain 3+:  Multiple layers nested.
           Like exp(sin(x)) or damped oscillators.
           Often wants float64. FPGA profiles need review.
           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 python,c --explain -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:  LOW            ← still validate the input range
  evidence:
    selected_targets: python, c
    hardware_profile: not requested in this lesson

Chain order 0 means this PID is just arithmetic. No exp. No sin. Pure math. That makes it easier to inspect, but deployment still needs tests for the numeric range you care about.

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
  review_note:  nested exp/cos path needs stronger numeric evidence

The compiler told you the complexity jumped. Before you ran anything expensive. Chain order is a review signal, not a proof of speed, stability, or deployability.

Proof-shaped obligations

Making the artifact state what must be proved

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 theorem-shaped scaffold 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)
  → "This is the safety property I want evidence for"
  → The artifact records a proof obligation for that property

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 is an explicit open obligation, not a proof claim.

Why this matters

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

WITH @verify:
  "The generated theorem states exactly what must be proved."
  "A checked proof can close the obligation later."
  "The claim boundary is visible instead of hidden."

Advanced preview: other proof targets

The same obligation shape can be routed to other proof-shaped or contract-shaped targets where those local backends are enabled. Each target still needs its own validation; emitting a scaffold is not the same thing as discharging a proof.

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-shaped preview

Preparing your math for hardware review

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
}

Emit a hardware-shaped artifact

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 (estimate)
    DSP blocks: 2
    exp units: 0 (not needed — chain 0)
    clock:     100 MHz
    latency:   estimate only
    utilization: planning estimate only

A selected hardware-shaped artifact may look like:

verilog// Generated by EML-lang Verilog backend
// Chain order: 0 | planning profile only

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 candidate. The next steps are simulation, synthesis, board integration, and an evidence packet before any hardware-deployment claim.

What the numbers mean

LUTs:      Estimated logic blocks for the selected FPGA profile.
           Treat this as a planning signal until synthesis confirms it.

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

Latency:   Estimated clock cycles from input valid to output valid.
           Simulation and synthesis must confirm timing.

For comparison:
  Software path: run and test first.
  FPGA path:     emit, simulate, synthesize, then measure.

  Do not claim speed until measured evidence exists.

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 the selected lesson artifacts

bashpython tools/cli/main.py my_project.eml --target python,c --explain -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 proof-shaped obligations (@verify) without claiming proof
  6. Previewed a hardware-shaped profile (@target) without claiming hardware validation
  7. Built YOUR OWN bounded artifact

You can now:
  - Write any equation in EML-lang
  - Emit selected software artifacts for inspection
  - Read the structural profile (chain order, drift risk)
  - State proof obligations for later proof work
  - Prepare hardware candidates for simulation and evidence review

One equation. Inspectable artifacts. Explicit evidence boundaries.

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")  record a proof-shaped obligation
  @target(fpga, clock_mhz = N)     record a hardware-shaped profile
  requires CONDITION               input precondition
  ensures  CONDITION               output postcondition

COMPILE
  python tools/cli/main.py file.eml --target python,c -o ./out
  python tools/cli/main.py file.eml --target c -o out.c
  python tools/cli/main.py file.eml --target lean -o out.lean       preview scaffold
  python tools/cli/main.py file.eml --target verilog -o out.v       preview artifact

PROFILE READING
  chain_order: 0   polynomial (usually low drift risk)
  chain_order: 1   exponential (check domains and exponent size)
  chain_order: 2   trigonometric (sample-grid checks recommended)
  chain_order: 3+  nested (stronger numeric review recommended)
  drift_risk: LOW / MEDIUM / HIGH  precision warning

You finished. Now what?

1. Build one bounded packet. Take one equation from this lesson, emit selected Python/C artifacts, save the chain-order profile, and write down which claims are still blocked.

Open the packet builderContinue to the first guard kernel