Correct by construction#

There is no NULL pointer, no exception to forget, and no case left unhandled. If a Geng program compiles, those crashes cannot happen. What can still go wrong?

Runtime asserts, moved to compile time#

Other languages check many things with an assert while the program runs: is this index in range? is this array empty? is this number between 0 and 100? can this sum overflow? In Geng these rules go in a function’s type, and the compiler checks every call against them before the program is built. You check once where the data comes in, and the compiler proves the rule holds everywhere after that. Code past that point doesn’t repeat the check, doesn’t slow down for it, and can’t forget it.

A rule can sit on a type, too: every place that builds or changes a value of that type must prove the rule holds, and every place that reads one can rely on it. This is the screen of puritty, a terminal emulator written in Geng, cut down to its layout: one flat buffer of cells. The rule after where is written once. The compiler checks it everywhere a Screen is built or changed, and knows it everywhere one is read. From it, the compiler proves that slot lands inside the ring, that rowOffset leaves room for a whole row (multiplying two values, without overflowing), and that cellAt reads inside the buffer, with no test at run time. Take stride == cols + 1 out of the rule, and the program no longer compiles. In puritty itself, every read of a screen row is proved this way. See Refinement types.

type alias Screen =
    { cells : Builder Int64
    , cols : Int
    , rows : Int
    , stride : Int
    , base : Int
    , size : Int
        where 1 <= cols && 1 <= rows && rows <= size && stride == cols + 1
            && 0 <= base && base < size && Builder.length cells == size * stride
    }


-- Where row `y` is in the ring.
slot : (s : Screen) -> (y : Int where 0 <= y && y < s.rows) -> (r : Int where 0 <= r && r < s.size)
slot s y =
    if s.base >= s.size - y then
        s.base - (s.size - y)

    else
        s.base + y


-- Where row `y` starts in the buffer: a whole row always fits after it.
rowOffset : (s : Screen) -> (y : Int where 0 <= y && y < s.rows) -> (r : Int where 0 <= r && r + s.stride <= Builder.length s.cells)
rowOffset s y =
    slot s y * s.stride


-- So reading a cell needs no bounds check and no Maybe.
cellAt : (s : Screen) -> (y : Int where 0 <= y && y < s.rows) -> (x : Int where 0 <= x && x < s.cols) -> Int64
cellAt s y x =
    Builder.getProven (rowOffset s y + x) s.cells

Geng is not a proof assistant like Lean or Rocq. You don’t write proofs, and the compiler doesn’t claim your program does what you meant. Its rules are refinement types, the approach of Liquid Haskell and Flux for Rust: a rule is a condition on a value, and a solver checks it with no proof written by hand. Geng’s solver reasons about whole numbers (lengths, indexes, counts and ranges), and when it can’t show a rule holds, the program doesn’t build.

A report for you, and for your LLM#

Code an LLM writes compiles, reads well, and can still hide a Maybe.withDefault 0 that has a code smell. The checks report (coming soon) lists what the compiler proved, function by function. It also lists every fallback in the program, a Nothing branch or a default value, and says which ones can never run and which ones can. You can see where the program relies on a proof and where it relies on a fallback, without reading every line. The same report is something the LLM can act on: turn a reachable fallback into a rule the compiler checks, build again, and watch the count go down.

From the report for puritty, a terminal emulator written in Geng:

The first is the EUC-KR decoder: its table read is proved in range, because the decoder’s state carries a rule the compiler checks at every step. The last is a fallback that runs by design, when an escape sequence leaves out its parameter, and the report shows the values that reach it so you can decide that at a glance.

Reliable everywhere#

One program, the same behavior on every target.

Native	Erlang BEAM	JavaScript	WebAssemblyComing soon	JVMComing soon
for speed	for extreme uptime	browser and Node.js	anywhere WASM runs	for interop

See Platforms and targets.

Get started · Geng is not released yet; see Status and roadmap.

Geng started as a fork of Gren, which is itself a fork of Elm. We thank everyone who has contributed to those languages: without them, we would not have had such a strong foundation.