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 as much checking as it can into the compiler, so a program is checked before it runs, not while it runs. That matters more now that LLMs write much of our code.
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.
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?
Checked before it runs#
Many checks that other languages make while the program runs (is this index in range? is this list empty? is this value valid?) can be done by the Geng compiler. You write the rule in the type, check it once where the data comes in, and the compiler proves it holds everywhere else. Code past that check doesn’t repeat it, 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"
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. Yes, you can assert this at run time in any
language, but Geng enforces it at compile time. See
Refinement types.
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 |
Get started · Geng is not released yet; see Status and roadmap.