Tell us about capability-safety. Tell us about how you'll avoid plan interference. Tell us about about what makes this language fundamentally safe and not just hard-to-use.
Sure. For example, you might specify a contract which happens to require a solution to a Diophantine equation be generated for a certain handful of coefficients. This is known to scale up in complexity to Turing-completeness. [0] An example equation might govern the exchange or transfer of some resources, in which the contract only accepts a resource exchange which is equivalent in value.
A broadcast-ledger type currency requires every node to agree on the outcome of running transaction scripts. This is very impossible if running scripts is undecidable.
Even in this... implausible scenario, the contract would only need to verify the solution to the equation. The party creating the transaction would then be responsible for generating a solution.
A step in the right direction. I'm still waiting for a TLA+-like language where you can build proofs for high level custom properties like "Robust to some parts of the contract being indefinitely delayed".
15 comments
[ 2.6 ms ] story [ 41.4 ms ] thread[0] https://en.wikipedia.org/wiki/Hilbert's_tenth_problem
amountRequired: Amount amountNeeded: Amount
then...
verify amountRequired * 3 == amountNeeded
Any ideas?