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

Install the compiler once — it is free, and every target is included:

bashpip install monogate-forge

Then compile. Each command takes one source and one target:

basheml-compile hello.eml --target python -o hello.py
eml-compile hello.eml --target c -o hello.c

What you get

hello.py          ← Python
hello.c           ← C

Want every target at once? eml-compile hello.eml --target all -o my_first writes one file per target into my_first/ and skips the targets whose annotation the source does not carry.

Open hello.c and look (file header trimmed):

hello.c#include "libmonogate.h"
#include <stdint.h>
#include <math.h>

/*
 * add
 * Pfaffian chain count (eml-cost pfaffian_r): 0     Cost class: p0-d1-w0-c0
 * EML depth:   1  Symbolic band: LOW (from pfaffian_r only)
 * Numerical:   cancellation exposure NONE  (no mixed-sign subtraction)
 * Dynamics:    0 osc, 0 decay  (predicted_r=0)
 * obligations for add: none declared (this artifact proves well-typedness only)
 * FPGA est:   1 MAC, 0 exp, 0 ln, 0 trig -> 2 cy @ 32-bit
 */
double add(double a, double b) {
    return (a + b);
}

Your equation, lowered into C. libmonogate.h ships inside the monogate-forge package, under software/runtime/c/.

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                 co   pfaffian_r
──────────────────────────────────────────────────────────────
+ - * /        arithmetic                   0    0
exp(x)         e to the x                   1    1
ln(x)          natural log of x             1    1
sqrt(x)        square root                  1    1
pow(x, y)      x to the y                   1    1
pow(x, 2.0)    constant whole exponent      0    1
tanh(x)        hyperbolic tangent           1    1
eml(x, y)      exp(x) - ln(y)               1    2
sin(x)         sine                         2    2
cos(x)         cosine                       2    2
tan(x)         tangent                      2    1
atan2(y, x)    angle from coordinates       2    0
arcsin(x)      inverse sine                 3    0
arccos(x)      inverse cosine               3    0
abs(x)         absolute value               0    0
clamp(x, l, h) clip to range                0    0
min(a, b)      smaller of two               0    0
max(a, b)      larger of two                0    0

These are the two numbers --profile-only prints for a function whose body is one such call: co, the chain order the language spec defines, and pfaffian_r, the Pfaffian chain count eml-cost derives. They are not the same number, and nesting is not addition: exp(sin(x)) is co 3, but a product of two of them is the larger of the two, not the sum.

Compile and read the profile

basheml-compile transcendental.eml --profile-only

The compiler tells you about each function (two of the three shown):

# Module: (unnamed)  (3 fn, 0 const, 0 type)
# Source: transcendental.eml
# co: chain order (lang/spec/types/chain_order_types.md)    pfaffian_r: eml-cost's Pfaffian chain count

  exponential_decay
    status: ok    co: 1    pfaffian_r: 1    cost_class: p1-d2-w1-c0    eml_depth: 2    drift: MEDIUM
    dynamics: 0 osc, 1 decay  (predicted_r=1)
    fpga: 2 MAC, 1 exp, 0 ln, 0 trig (4 cy @ 32-bit)

  damped_wave
    status: ok    co: 2    pfaffian_r: 3    cost_class: p3-d5-w2-c0    eml_depth: 5    drift: HIGH
    dynamics: 1 osc, 1 decay  (predicted_r=3)
    fpga: 5 MAC, 1 exp, 0 ln, 1 trig (10 cy @ 64-bit)

exponential_decay has one exp layer, so chain order 1. damped_wave multiplies an exp by a cos: the chain order is the larger of the two, 2, while the Pfaffian chain count is 3 — the cos carries its own sin — and the drift flag rises with it.

What chain order means (plain English)

Chain 0:   Just arithmetic. x + y, x * y, pow(x, 2.0).
           Usually simplest. Low drift risk on normal ranges.
           Still validate your numeric range.

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

Chain 2:   Trig involved. sin, cos, tan, atan2.
           Like oscillations, waves, rotations. A damped
           oscillator (exp times cos) is still chain 2.
           Usually wants float32+ and sample-grid checks.

Chain 3+:  Layers nested, or an inverse trig function.
           Like exp(sin(x)), arcsin(x), arccos(x).
           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

basheml-compile pid_controller.eml --target python -o pid_controller.py
eml-compile pid_controller.eml --profile-only

What the compiler tells you

# Module: (unnamed)  (1 fn, 3 const, 0 type)
# Source: pid_controller.eml
# co: chain order (lang/spec/types/chain_order_types.md)    pfaffian_r: eml-cost's Pfaffian chain count

  pid
    status: ok    co: 0    pfaffian_r: 0    cost_class: p0-d2-w0-c0    eml_depth: 2    drift: LOW
    dynamics: 0 osc, 0 decay  (predicted_r=0)
    fpga: 2 MAC, 0 exp, 0 ln, 0 trig (4 cy @ 32-bit)

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
}

Profile it again:

basheml-compile nonlinear_pid.eml --profile-only

  adaptive_pid
    status: ok    co: 2    pfaffian_r: 3    cost_class: p3-d5-w2-c0    eml_depth: 5    drift: HIGH
    dynamics: 1 osc, 1 decay  (predicted_r=3)
    fpga: 5 MAC, 1 exp, 0 ln, 1 trig (10 cy @ 64-bit)

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 code state what must be true

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  (result >= -max_output)
    ensures  (result <= max_output)
{
    clamp(Kp * error + Ki * integral, -max_output, max_output)
}

What the new keywords mean:

@verify(lean, theorem = "pid_is_bounded")
  → "Emit a Lean theorem for this function, and try to prove it"
  → 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 (result >= -max_output)
ensures (result <= max_output)
  → "This is the property the theorem states"
  → One conclusion per ensures

Compile to Lean

basheml-compile safe_pid.eml --target lean -o ./safe_pid.lean

Open safe_pid.lean (imports trimmed):

leannoncomputable def safe_pid (error : Real) (integral : Real) : Real :=
  (max (-max_output) (min ((Kp * error) + (Ki * integral)) max_output))

theorem pid_is_bounded (error : Real) (integral : Real)
    (h1 : ((abs error) < (50.0 : Real)))
    (h2 : ((abs integral) < (500.0 : Real)))
    (h_clamp1 : (-max_output) ≤ max_output) :
    (((safe_pid error integral) >= (-max_output))) ∧ (((safe_pid error integral) <= max_output)) := by
  unfold safe_pid
  try unfold Kp at *
  try unfold Ki at *
  try unfold max_output at *
  try mach_split_hyps
  try dsimp only
  all_goals
    (try simp only [add_zero, zero_add, mul_zero, zero_mul, mul_one_ax, one_mul_thm, div_one_eq, ofSci_zero]) <;> refine ⟨?_, ?_⟩ <;>
      first
      | (apply lo_le_clamp <;> (first | assumption | mach_positivity))
      | (apply clamp_le_hi <;> (first | assumption | mach_positivity))
      -- ... 14 more tactics, tried in order ...
      | sorry  -- out of reach; left for the prover

One hypothesis per requires, one conclusion per ensures. Forge adds h_clamp1 itself: a clamp needs its lower bound not above its upper bound.

Is it proved?

Do not look for sorry. It is always there: Forge emits a list of tactics to try in order, and sorry is the last one, reached only if all the others fail. Ask Lean what the theorem depends on instead. That needs MachLib, the Lean library these theorems are stated against:

bashgit clone https://github.com/agent-maestro/machlib
cd machlib/foundations
lake build          # needs elan; about ten minutes the first time
echo '#print axioms pid_is_bounded' >> /path/to/safe_pid.lean
lake env lean /path/to/safe_pid.lean

'pid_is_bounded' depends on axioms: [propext, Classical.choice, Real, Quot.sound,
 addR, leR, le_iff_lt_or_eq, ltR, mulR, negR, realOfScientific, zeroR]

No sorryAx in the list, so pid_is_boundedis proved. The list is what the proof rests on: Lean's own propext, Classical.choice and Quot.sound, plus MachLib's axioms for the real numbers.

True is not the same as proved

Delete the clamp and return Kp * error + Ki * integral. The theorem is now false: at error = 49 and integral = 499 the output is 172.4. Recompile, and #print axioms shows sorryAx.

Now tighten the inputs to abs(error) < 20.0 and abs(integral) < 400.0. The output stays under 90, so the theorem is true again, and it still shows sorryAx: none of the tactics Forge tries finds this proof. sorryAx means not proved. It does not mean false.

Why this matters

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

WITH @verify:
  "The theorem states exactly what must be true."
  "#print axioms says whether it is proved."
  "An unproved theorem 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.

basheml-compile safe_pid.eml --target coq      -o ./safe.v
eml-compile safe_pid.eml --target isabelle -o ./Safe.thy
eml-compile 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

basheml-compile fpga_pid.eml --target verilog -o pid.v
eml-compile fpga_pid.eml --target systemverilog -o pid.sv
eml-compile fpga_pid.eml --allocate

The compiler does not create directories, so write to pid.v or make the folder first. --allocate prints the plan:

  FPGA allocation plan for Arty A7-100
  EML depth:      2 (a resource estimate, not latency)
  Clock target:   100 MHz
  Timing:         not modeled here (see the emitted RTL)

  Resources:    100 LUTs     2 DSPs      0 KB BRAM
  MAC units:  2
  Transcendental units: none (pure-polynomial design)

The start of pid.v:

verilog// Target device: Arty A7-100
// EML depth:    2 (a resource estimate, not latency)
// Estimated:    100 LUTs, 2 DSPs, 0 KB BRAM
// Clock target: 100 MHz (the plan does not model timing)

`default_nettype none

// Pipeline: hardware_pid
// Pfaffian chain count (eml-cost pfaffian_r): 0     Cost class: p0-d2-w0-c0
// EML depth:   2  Width: 32 bits
// Total latency: 3 cycles (2 internal + 1 output reg)
// Throughput:    a new sample on every clock edge (100 Msamples/s at 100 MHz)
module hardware_pid_pipeline #(
    parameter WIDTH = 32,
    parameter FRAC  = 16
) (
    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
);

    localparam signed [WIDTH-1:0] Kp = 32'sd163840;  // 2.5
    localparam signed [WIDTH-1:0] Ki = 32'sd6554;  // 0.1
    // ...
    assign _w1_full = Kp * error;
    assign _w2 = _pr1 >>> FRAC;

The gains became Q16.16 fixed-point constants, and each product is shifted back down by FRAC bits.

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

EML depth: The allocator's resource estimate, NOT a latency and not a
           throughput. 0.14.4 called it "Pipeline depth" and divided the
           clock by it to print "50.0 Msamples/s"; that number was wrong.
           Simulated, pid.v takes a new sample on every clock edge and
           answers 3 cycles later, so it runs at the clock rate. 0.15.0
           and 0.16.0 print "Timing: not modeled here" in the plan and
           put the real "Total latency: 3 cycles" in the RTL header.
           Whether a part closes timing at 100 MHz is for synthesis to say.

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 it

basheml-compile my_project.eml --target python -o my_project.py
eml-compile my_project.eml --target c -o my_project.c
eml-compile my_project.eml --target lean -o my_project.lean
eml-compile my_project.eml --target verilog -o my_project.v

Then run #print axioms force_proportional as in Lesson 4. With monogate-forge 0.16.0 it shows sorryAx: the bound is true (the output stays under 1000 + 500) but not proved. Can you rewrite the function so it is?

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. Stated a property with @verify and asked Lean whether it is proved
  6. Emitted 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 software targets, one per command
  - Read the structural profile (chain order, drift risk)
  - Tell a proved theorem from a stated one with #print axioms
  - 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")  emit a Lean theorem and try to prove it
  @target(fpga, clock_mhz = N)     emit a hardware-shaped profile
  requires CONDITION               input precondition
  ensures  CONDITION               output postcondition

COMPILE (one source and one target per command)
  eml-compile file.eml --target python -o out.py
  eml-compile file.eml --target c -o out.c
  eml-compile file.eml --target lean -o out.lean     # needs @verify(lean)
  eml-compile file.eml --target verilog -o out.v     # needs @target(fpga)
  eml-compile file.eml --target all -o out           # every target it qualifies for
  eml-compile file.eml --profile-only                # chain order, cost class, drift

CHECK A PROOF (in machlib/foundations)
  echo '#print axioms NAME' >> /path/to/out.lean
  lake env lean /path/to/out.lean    # sorryAx in the list = not proved

PROFILE READING
  co: 0    polynomial (usually low drift risk)
  co: 1    exponential, sqrt, pow, tanh (check domains and exponent size)
  co: 2    trigonometric (sample-grid checks recommended)
  co: 3+   nested, or inverse trig (stronger numeric review recommended)
  pfaffian_r: N   eml-cost's Pfaffian chain count; not the same as co
  drift: LOW / MEDIUM / HIGH  precision warning

You finished. Now what?

1. Prove one property. Take one equation from this course, give it requires and ensures, compile it to Lean, and check with #print axioms whether it is proved.

Continue to the first guard kernel