2 A first program — build, run, get rejected

2.1 Building the tool#

The compiler is called lowentc. After getting the repository, build it in impl/. All you need is a C compiler that knows C23 (gcc or clang) and make.

cd impl
make            # build/lowentc
make check      # unit tests and standard-library checks

When make finishes there is an impl/build/lowentc. Commands in this book are written as lowentc, assuming it is on your path.

2.2 hello, entropy#

The smallest program that prints.

module hello .
rem run: main

proc main input out cap io . output u8 . effects io . do
  return narrow u8 (write_out out 1 "hello, entropy!\n") .
end

$ lowentc --run main hello.low
hello, entropy!
main() = 16

The first line, module hello ., is the module declaration every file opens with. The rem on the second line is a line comment; in this book it tells the verification script what to do.

Read the head one clause at a time.

• proc main — an impure op named main. Output leaves a trace outside, so it cannot be a fn.
• input out cap io . — receives an io capability named out. It is needed to write to standard output.
• output u8 . — returns a u8.
• effects io . — declares that it performs input/output.

The body lies between do and end. write_out out 1 "…" takes the capability out as its first argument, writes bytes to file descriptor 1 (standard output), and returns the number of bytes written. hello, entropy!\n is 16 bytes, so it returns 16. That is narrowed to fit a u8 with narrow u8. Narrowing carries a check that stops execution if the value does not fit (chapter 4).

The last line of the output, main() = 16, is the line where the VM shows the op’s return value.

2.3 Running it two ways#

--run ran it on the virtual machine inside the compiler. To run the same program natively, emit C and build it with a C compiler.

lowentc --emit-c hello.low > hello.c
cc -O2 -o hello hello.c -lm
./hello main

The native executable takes the name of the op to run as its first argument. Running main prints the same line, and the return value 16 comes out as the process exit code (see it with echo $?). That is why main’s output is u8 — an exit code is one byte.

Slice arguments are given in brackets. The next op computes the mean of a byte slice.

module stats .
rem run: mean [3,4,8]

fn mean input xs slice u8 . output u64 .
  requires gt (len xs) 0 .
do
  var total u64 be 0 .
  for x xs do
    set total (add total (widen u64 x)) .
  end
  return div total (len xs) .
end

$ lowentc --run mean stats.low [3,4,8]
mean([3,4,8]) = 5
  arg0 (written) = [3,4,8]

requires gt (len xs) 0 . is a contract. The caller promises not to pass an empty slice. Because of that promise, the body’s div total (len xs) need not worry about dividing by zero. The line arg0 (written) = [3,4,8] below the result is the VM showing the final state of the slice argument.

2.4 How a contract stops execution#

What happens if a contract is broken? The next op only accepts values up to 100.

module doubling .
rem run: twice 21
rem test

export fn twice input n u32 . output u32 .
  requires le n 100 .
do
  return mul n 2 .
end

test twice_works
do
  expect eq (twice 5) 10 .
  expect eq (twice 0) 0 .
end

$ lowentc --run twice twice.low 21
twice(21) = 42
$ lowentc --test twice.low
  [PASS] twice_works
== tests: 1 run, 1 passed, 0 FAILED ==

Give it a value that breaks the promise, as in lowentc --run twice twice.low 200, and the VM stops before entering the body with E-VM-CONTRACT: requires violated at entry. If the argument is written as a constant in a call (twice 250), there is no need to run at all — --check rejects it with E-CONTRACT-IMPOSSIBLE. A contract is not a comment.

The test twice_works block in the same file is a test. expect is the assertion, and --test runs every test block. The last two lines of output are its result. --check does not run tests — passing the check does not mean the tests passed, so running --check on a file with tests produces a W-TEST-NOT-RUN warning to say so.

2.5 Getting rejected#

A good part of the time spent learning Lowent is time spent being rejected by the compiler. Rejection is not punishment but conversation. Every diagnostic carries a stable code, and that code keeps its meaning across releases.

module twice_bad .
rem expect: E-EFFECT-CALC

fn shout input out cap io . output u64 .
do
  return write_out out 1 "hi\n" .
end

$ lowentc --check twice_bad.low
twice_bad.low:5:1 E-EFFECT-CALC: this fn is declared pure but performs `io` — make it a `proc` with `effects …`, or remove the effect

A diagnostic line has the shape file:line:column code: explanation. In this example fn shout is declared pure but its body does input/output with write_out. The compiler rejects it with E-EFFECT-CALC and names two ways to fix it — make it a proc with effects, or remove the effect.

With --diag-json the same diagnostic comes out as one line of JSON. The rule code (rule), location (span) and the name of the repair (repair) are separate fields, so an editor or an AI can tell what is wrong without picking the prose apart.

{"rule":"E-EFFECT-CALC","sev":"error","phase":"effect", … ,"repair":"R-CALC-TO-PROC"}

2.6 --fmt fixes the shape#

The clauses of an op head are written in one fixed order. Inputs come before the output. A wrong order is rejected.

module messy .
rem expect: E-CLAUSE-ORDER

fn area output u64 . input w u64 . input h u64 .
do
  return mul w h .
end

$ lowentc --check messy.low
messy.low:4:22 E-CLAUSE-ORDER: a data input comes after `output`. An op header has ONE order: `satisfies`/`lowdoc` · `vector`/`priority` · `comptime` inputs · capability/region inputs · `using` · data inputs · `output` · `effects` · `link`/`variadic` · `asm` · `access`/`inplace`/`invalidates`/`parallel`/`reduce` · `requires` · `ensures` · `errors` · `tests` (`--fmt` moves the non-input clauses for you; inputs are call positions, so reorder those and their call sites yourself)

The long explanation in the diagnostic is the order table itself. The whole of it is covered in chapter 3 for now remember one thing: --fmt moves clauses that are not inputs (output, effects, contracts and so on) into place. It does not reorder inputs among themselves. The order of inputs is also the order of arguments at every call site, so moving them would change every call.

The canonical form --fmt prints puts one clause per line and shows every parenthesis. Nobody has to write in that shape. The canonical form is the yardstick a machine uses to compare whether two pieces of code mean the same.

2.7 Arguments and capabilities#

Reading program arguments is a capability too. The next program greets its first argument.

module greet .
rem (argument numbering differs between native and VM, so this is only checked)

proc main input out cap io . input a cap args . output u8 . effects io .
do
  let who option slice u8 be arg a 0 .
  guard is_some who . else return narrow u8 (write_out out 1 "no name\n") .
  let n u64 be write_out out 1 "hello, " .
  let m u64 be write_out out 1 (some_value who) .
  let k u64 be write_out out 1 "\n" .
  return 0 .
end

$ lowentc --check greet.low
== check: ok ==

input a cap args . receives the argument capability, and arg a 0 reads the first argument. There may be no argument, so the result is option slice u8. guard is_some who . else … leaves on the spot when there is no value, and below it you may trust that the value exists (chapter 11). Capability inputs come before data inputs, and the two capabilities take argument positions in the order written.

Note that the single line effects io . covers both capabilities. args is a capability that can be read without an effect. How capabilities pair with effects is tabulated in chapter 16.

2.8 Common mistakes#

These are the rejections and stops you meet most often in a first program. When you see one of these codes, come back here.

module mistake_noend .
rem expect: E-BLOCK-UNCLOSED

proc main input out cap io . output u8 . effects io .
do
  let n u64 be write_out out 1 "hi\n" .
  return narrow u8 n .
rem ✘ the `do` that opened the body has no matching `end`

$ lowentc --check mistake_noend.low
5:1 E-BLOCK-UNCLOSED: missing 'end' for do-block

module mistake_nocap .
rem expect: E-EFFECT-NO-CAP

rem ✘ declares `io` but never receives the right to do it (`cap io`)
proc main output u8 . effects io .
do
  let n u64 be write_out 1 "hi\n" .
  return narrow u8 n .
end

$ lowentc --check mistake_nocap.low
mistake_nocap.low:5:0 E-EFFECT-NO-CAP: this op declares the `io` effect but receives NO capability that authorizes it. `io` is a cap-effect (RFC-0007 §6.7): I/O is a RIGHT you are HANDED, not an ambient power — `input fs cap file_system .` (or another `cap …` input). An effect you declare but hold no capability for is a claim the signature cannot back

module mistake_exitcode .
rem trap: main

proc main input out cap io . output u8 . effects io .
do
  var n u64 be 0 .
  var i u64 be 0 .
  while lt i 8 . do
    set n (add n (write_out out 1 "32 bytes of text on every line.\n")) .
    set i (add i 1) .
  end
  rem ✘ 256 bytes were written --- an exit code is one byte (0 … 255), so it does not fit
  return narrow u8 n .
end

$ lowentc --run main mistake_exitcode.low
32 bytes of text on every line.
32 bytes of text on every line.
32 bytes of text on every line.
32 bytes of text on every line.
32 bytes of text on every line.
32 bytes of text on every line.
32 bytes of text on every line.
32 bytes of text on every line.
== ir diagnostics (1) ==
0:0 E-VM-CAST: value does not fit the target width (use narrow_wrap / narrow_sat / narrow_try)

module mistake_opname .
rem trap: mian

proc main input out cap io . output u8 . effects io .
do
  let n u64 be write_out out 1 "hi\n" .
  return narrow u8 n .
end

$ lowentc --run mian mistake_opname.low
== ir diagnostics (1) ==
0:0 E-VM-UNDEF: no such op

2.9 This chapter’s syntax at a glance#