This is not so much of a blog post as it is notes for myself.
My quest for many years now has been to create a specific kind of specification language that would describe distributed systems, or in other words, multi agent systems, mainly human agents augmented by their computer devices.
Now here is an interesting thing. Let us assume that we do create such a language. How will be sure that the specification is respected by all participants?
For blockchains like Ethereum that have a weak type system, thus they do not have a specification language, the only way to trust the computation is to actually perform the computation in the public.
This does not have to be the case for us. A specification in a dependent type language does require computation to determine the type of the output of a function, but it does not require to know the function itself, just its type. Thus one could have a private function that computes a value, and that value can be checked against its expected type.
In other words, all we need is to compute the types of the outcomes of a computation to provide validation. This is huge because we can then abstract big parts of a distributed system, like a group of actors, and simply forget about its internal structure. Our only concern would then be the validation of the results at the edges with the outside world.
This can enable a hierarchical decentralized validation mechanism, where a single centralized blockchain is not needed.
( We do need to make sure that each abstract function is not called more than once with the same input, because then we would have to also check that they give back the same value, and we do not want to do that.)
