Functional WebAssembly is an experimental functional programming language that compiles directly to WebAssembly. It is based directly on Lambda Calculus functions for its different contructs and aims to allow for mathematically sound and thus proveable code. It is not directly solely at the web but at any runtime that can handle WebAssemlbly bytecode.