For some applications (notably blockchains with a consensus algorithm) it is important to ensure that the contract logic is deterministic.
While Ergo is designed to be deterministic, it would be useful to document the approach and possible source of concerns and address them.
Some initial thoughts
Ergo is functional, cannot use data which is not in its input, every operation within the language is deterministic
The official semantics in Coq is deterministic, and the source of truth for what programs mean
Deterministic is defined with (an implicit or explicit) equality in mind: for all inputs input1 and input2 and ergo invocation of a clause f, input 1 = input 2 -> invoke f (input1) = invoke f (input2)
Determinism isn't just a factor of the source language semantics, since we are compiling we also want to guarantee that the compiled code (for all supported target runtimes) preserves that semantics (modulo the above equality)
We rely on some runtime libraries in some cases (the main of those for the JavaScript backend is momentjs)
We rely on a specific version of a specific execution environment (e.g., what happens when node.js fixes a bug? and users may depend on different versions?)
Some possible aspects that may need review wrt to determinism
Implementations of IEEE arithmetics are free to return -NaN or +NaN as they wish. Remark: those should be considered equal!
jeromesimeon
commented
4 years ago
Description
For some applications (notably blockchains with a consensus algorithm) it is important to ensure that the contract logic is deterministic.
While Ergo is designed to be deterministic, it would be useful to document the approach and possible source of concerns and address them.
Some initial thoughts
input1andinput2and ergo invocation of a clausef,input 1 = input 2 -> invoke f (input1) = invoke f (input2)momentjs)Some possible aspects that may need review wrt to determinism
-NaNor+NaNas they wish. Remark: those should be considered equal!