use lowercase ascii identifiers with underscores. type annotations follow the form:

function_name(arg1: type1, arg2: type2): return_type

all operations use explicit prefix calls:

contains(set, element)
product(type_a, type_b)

functions are total and context-free. no overloading. no implicit dependencies.

function root_group(p: potential): group =
  find_shallowest(mounted_groups(p))

type group:
  id: string
  start_time: time
  duration: time

module potential_mounting:
  function referenced_groups(p: potential): list = ...
  function root_group(p: potential): group = ...

trait group_homomorphism:
  function map(x: group_elem): group_elem

allow let, match, and block structure.

potential_analysis:
  function evaluate_window(p: potential): (time, duration) =
    let g = root_group(p)
    in (g.start_time, g.duration)

desugaring:

match r as t:
  f1 = ...
  f2 = ...
->
let f1 = r.f1
let f2 = r.f2

replace symbolic quantifiers with iteration:

for x in domain: ...
exists y in domain: ...

arrays are typed functions:

a: function(i: int, j: int): real

explicit index binding:

sum(i: 1..n, a(i, j) * b(j, k))

desugaring:

sum(i: 1..n, expr)
->
sum(i in range(1, n), expr)

a[i][j]
->
a(i, j)

compose(f, g)(x)
->
f(g(x))

pipe(x, f, g)
->
g(f(x))

use named expressions:

delta(x) = (x, x)
pair(x) = (x, f(x))

fully parenthesize:

sub(add(1, div(mul(2, pow(c, d)), e)), f)

filter(x in domain, condition)
->
filter(domain, function(x): condition)

avoid "...":

sequence(n: int): list = map(i: 1..n, i)

tagged sum types:

type expr =
  | number(value: real)
  | variable(name: string)
  | binary(op: operator, left: expr, right: expr)

function(x): expr
->
lambda_expr(param = x, body = expr)

function f(x: t): u
  precondition: p
->
function f(x: t): u?
  if p then return 

real?
->
optional

predicate is_prime(n: int): bool
proof: exists p in primes: divides(p, n)

function safe_div(x: real, y: real): real?
  if y ≠ 0 then return x / y

symbolic forms must expand to referential form:

notation: "⟨x, y⟩" maps to inner(x, y)

φ: map g -> h where φ is group_homomorphism
->
φ: function(x: group_elem): group_elem
  satisfies group_homomorphism

epsilon-delta definition:

for epsilon in positive_reals:
  exists delta in positive_reals:
    for x in reals:
      if 0 < abs(x - c) and abs(x - c) < delta:
        abs(f(x) - l) < epsilon

matrix multiplication:

c(i, k) = sum(j: 1..n, a(i, j) * b(j, k))

set-builder:

filter(x in naturals, exists y in naturals: y * y = x)

inner product:

inner(x: vector, y: vector): scalar =
  sum(i: 1..n, x(i) * y(i))

pointwise equality:

functions_equal(f, g, domain) =
  for x in domain:
    f(x) = g(x)

• function application
• type definitions
• lexical blocks
• iteration
• conditionals
• lambda expressions
• primitive data and operators all other forms desugar to these.