Correct by construction. Reliable everywhere.

“A craftsman who wants to do his work well must first sharpen his tools.”

工欲善其事，必先利其器。

— Confucius 孔子, Analects 论语

Speed is easy to measure. Correctness is harder, and it matters more: a fast program you can’t trust is no use. Geng is a small, pure functional language that moves many of the checks other languages make at run time into the compiler, so more of a program is checked before it runs, not while it runs. That matters even more now that LLMs write much of our code.

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.

-- The type says there is always at least one reading.
latest : (readings : Array Float where Array.length readings > 0) -> Float
latest readings =
    Array.getProven (Array.length readings - 1) readings

report : Array Float -> String
report readings =
    if Array.length readings > 0 then
        "Now " ++ String.fromFloat (latest readings) ++ "°C"

    else
        "No readings yet"

The latest function takes an Array Float, but not just any Array Float: only one that the compiler can prove has a length greater than zero. So latest reads the last element directly: no Maybe, no bounds check. The one check is in report, and the compiler sees it. Leave out the if, and the program does not compile: the error names the rule, the facts the compiler had, and values that would break it. See Refinement types.

Geng is not a proof assistant like Lean or Coq. 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:

$ geng checkspuritty · vt, the terminal core
107 checks hold 14 fallbacks never run 180 can run 14 open
Vt.Charset
checks holdgo1 read in range · 21 contract checks · 10 sums cannot wrap · 1 fallback never runs
Vt.View
never runscellAt:1092the default of withDefault is never used
opencellAt:1089row + x can wrap, when row = -2147483648, x = -1
Vt.Cursor
can runparam:86the Nothing branch runs when Array.length params = 0

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.

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