TECH

WHAT N2O REALLY IS?

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.

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）：

N2O.JS CLIENT

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）：

O7 ERLANG ELIXIR HAMLER

These repos are stable and mature.

synrc/n2o — N2O 7.12.0 Distributed WebSocket Server
synrc/kvs — KVS 7.11.5 Key Value Store
synrc/mad — MAD 7.1.1 Erlang Package Manager
synrc/bpe — BPE 5.12.0 Business Process Engine
synrc/nitro — NITRO 5.12.4 Nitrogen Web Framework
synrc/rest — REST 5.10
synrc/active — ACTIVE 4.11
synrc/fs — FS 4.10
synrc/exe — EXE 2.11
synrc/bert — RPC 1.11.1 Swift protobuf ASN.1 JavaScript
synrc/review — REVIEW 1.11 MQTT Chat with File Upload
synrc/sample — SAMPLE 1.11 WebSocket Chat with File Upload

Server Tier 1 — （SML、Haskell、F#、Rust）：

O1 STANDARD ML

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

O3 HASKELL

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

O83 RUST

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

o83/kernel — KERNEL SMP OS and K interpreter

Server Tier 0 — （Coq、Agda、Lean）：

O89 LEAN4

This is LEAN 4 N2O full-stack.

o89/n2o — N2O WebSocket Server
o89/nitro — NITRO Nitrogen Web Framework
o89/bum — BUM Lean4 Package Manager

O29 COQ

Coq.io based system-level Coq programming.

o29/n2o — N2O Coinductive Shell

HEART ADVICE

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.

LEGEND:

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）