Hermetic functions (or hermetic methods) are pieces of code that can modify only local state (including its arguments) to store the result of computation. They cannot modify global state (including thread-related state like mutexes) or make actual or virtual system calls (including allocating memory or querying timers). They can call other hermetic functions but any recursion must be declaratively finite (so that a worst case stack size requirement can be computed at compile time) and they cannot invoke user-supplied callbacks.
Hermeticity is similar to purity, although the exact definition of purity depends on who you ask. While pure functions are usually defined as without side effects, hermetic functions can modify its arguments' state (not just modify local variables).
For example, in Go notation, func pureSort(original []int) (sorted []int)
could take a slice of int
s and return a new slice containing the elements in sorted order - the original
slice is not modified. In comparison, func hermeticSort(dst []int, src []int) (dstWasLongEnough bool)
could copy src
's elements (in sorted order) to modify a caller-supplied slice dst
, provided that dst
was long enough.
This distinction is somewhat fuzzy if you think of the pass-a-dst
-slice mechanism as merely a performance optimization for ‘returning’ large values via an out parameter. Still, hermetic methods are allowed to modify the receiver argument's state, which is separate from return values or out parameters.
For example, func (otp *oneTimePad) Transform(dst []byte, src []byte, atEOF bool) (nDst int, nSrc int, err error)
could combine a one-time pad with an input stream, writing the result to an output stream. Calling Transform
performs some compute but it also updates the receiver otp
's state to track how much of the one-time pad remains after successive calls during streaming I/O. This Transform
method can be hermetic without being pure.
Hermeticity is similar to process-level sandboxing (like Linux's SECCOMP_MODE_STRICT
sandbox) but for hermetic functions, both caller and callee are in the same process. The motivation is the same - to compute on untrusted data without security-compromising surprises, even if there are bugs in the computation code - but the mechanism is different.
For seccomp
, the operating system enforces the restriction (at run-time) and communication (literally IPC or Inter-Process Communication) is heavyweight, asynchronous and complex.
For Wuffs, the compiler enforces memory-safety (at compile time) and communication (a function call) is lightweight, synchronous and simple. Wuffs the Language is deliberately unpowerful. There are:
unsafe
keyword,Wuffs is designed for writing hermetic, secure libraries, not complete programs, and with less power comes easier proof of safety.
In comparison to compiling C/C++ code with WebAssembly (which can be restricted to only compute), both Wuffs and Wasm allow for hermetic libraries within larger (memory-unsafe) C/C++ programs. The difference is that Wasm lets you re-use existing C/C++ libraries (albeit with a run-time performance penalty) but Wuffs performs on par with C code (albeit requiring re-writing those libraries).
Wuffs functions are not guaranteed to halt. We do not solve the Halting Problem. Furthermore, while there is a difference in theory between a function that doesn't halt and one that halts in 99 years, in practice there is not. Systems that already need to cope with the latter can also cope with the former.
Technically, ‘hermetic’ code can still affect other threads or processes indirectly: modifying what's in hardware caches, OS page tables or that spending CPU quota leads to a scheduler switch. Wuffs does not guarantee that code is safe from timing or speculative execution attacks. Nonetheless, Wuffs code does not have access to any clocks. Any Wuffs computation on “the current time” requires the caller to explicitly pass in that information.