N2O is a formal philosophy and software engineering exercise. It stricts you to be minimal and concise while remains functional and complete. It's a kind of purity discipline in software development. The application of the N2O method is modern web development: JavaScript, server-side DOM updates, binary protocols. N2O teaches how to write minimal and robust software.

N2O applications:

Formal spec for core libraries N2O, KVS and BPE in Anders language:

module N2O-KVS-BPE where import BASE axiom pickle : Binary -> Binary axiom depickle : Binary -> Binary axiom encode : Π (k: U), k -> Binary axiom decode : Π (k: U), Binary -> IO k axiom reg: Π (k: U), k -> IO k axiom unreg : Π (k: U), k -> IO k axiom send : Π (k v z: U), k -> v -> IO z axiom getSession : Π (k v: U), k -> IO v axiom putSession : Π (k v: U), k -> v -> IO v axiom getCache : Π (k v: U), Atom -> k -> IO v axiom putCache : Π (k v: U), Atom -> k -> v -> IO v axiom start : PI -> IO Sup axiom get : Π (f k v: U), f -> k -> IO (Maybe v) axiom put : Π (r: U), r -> IO StoreResult axiom delete : Π (f k: U), f -> k -> StoreResult axiom index : Π (f p v r: U), f -> Atom -> v -> List r axiom next : Reader -> IO Reader axiom prev : Reader -> IO Reader axiom take : Reader -> IO Reader axiom drop : Reader -> IO Reader axiom save : Reader -> IO Reader axiom append : Π (f r: U), f -> r -> IO StoreResult axiom remove : Π (f r: U), f -> r -> IO StoreResult axiom start : Proc -> IO Sup axiom stop : String -> IO Sup axiom next : ProcId -> IO ProcRes axiom amend : Π (k: U), ProcId -> k -> IO ProcRes axiom discard : Π (k: U), ProcId -> k -> IO ProcRes axiom modify : Π (k: U), ProcId -> k -> Atom -> IO ProcRes axiom event : ProcId -> String -> IO ProcRes axiom head : ProcId -> IO Hist axiom hist : ProcId -> IO (List Hist)

N2O blueprint implementations:

Client Tier 3 —(JavaScript、Lua):


ECMAScript client infrastructure for N2O full-stack specification.

  • UTF-8.JS — UTF-8 serialization
  • zlib.js — ZLIB inflate algorithm
  • IEEE-754.JS — Real Number Format serialization
  • BERT.JS — Binary Erlang Term Format serialization
  • N2O.JS — N2O/WebSocket JavaScript Client Loop
  • MQ.JS — N2O/MQTT JavaScript Client Loop
  • NITRO.JS — NITRO/JavaScript bindings of DOM sources
  • VALIDATION.JS — NITRO/JavaScript DOM sources validation

Server Tier 2 —(Erlang、Elixir):


These repos are stable and mature.

Server Tier 1 — (SML、Haskell、F#、Rust):


This is first System-F implementation for SML/NJ and MLton.

  • o1/n2o — N2O 0.11 WebSocket Server
  • o1/nitro — NITRO 0.11 Nitrogen Web Framework


This is second System-F implementation.

  • o3/n2o — N2O 0.11 WebSocket Server
  • o3/nitro — NITRO 0.11 Nitrogen Web Framework
  • o3/sample — SAMPLE 0.11 Simple Sample

O61 F#

This is third System-F implementation.

  • o61/ws — WS 1.0 WebSocket Server
  • o61/etf — ETF 1.0 Erlang Term Format Serializer
  • o61/nitro — NITRO 1.0 Nitrogen Web Framework


This is proof-of-concept of formal CPS interpreter with SMP runtime.

Server Tier 0 — (Coq、Agda、Lean):


This is LEAN 4 N2O full-stack.


Coq.io based system-level Coq programming.


Each language, N2O TECH is implemented in, should embed its philosophy most naturally and compact. If some layer between the base library of a language is needed, it could be provided, but it should be reduced to zero if possible. In some cases, some parts of a base library could be replaced with better replacement. N2O should provide client companion library usually implemented in a different set of client languages: JavaScript, Swift, Kotlin. If you did everything right, N2O should not be more than 500 LOC in any language.


  • Client Tier 3:(JavaScript、Lua)
  • Client Tier 2:(Swift、Kotlin、TypeScript)
  • Client Tier 1:(UrWeb、OCaml)
  • Client Tier 0:(Formality)
  • Server Tier 3:(PHP、Python、Perl、Ruby)
  • Server Tier 2:(Erlang、Elixir)
  • Server Tier 1:(Standard ML、Haskell、F#、Rust)
  • Server Tier 0:(Coq、Agda、Lean)