Quote from: monsterer on February 12, 2016, 01:23:17 PM

Quote from: TPTB_need_war on February 12, 2016, 12:55:41 PM

monsterer is wrong again. Even within the block there is no way to attain commutativity of ordering. Any particular choice of arbitrary orderings of script executions for a block result may achieve a different result for contracts than another ordering (unless the scripts are invariant to ordering but that basically means the scripts can do nothing). That is the definition of indeterminism.

Perhaps I should have said 'within one script execution within one block'. Block ordering is eventual, just like bitcoin. In ethereum this has scope for more dire consequences than it does with bitcoin; it depends on the application.

Specifically the generative essence distinction is that Bitcoin's UXTO history is a directed acyclic graph, which by definition means it has no recursion (i.e. no cycles).

Has anyone proven that Bitcoin's scripts maintain this property?

Whereas, only perfectly dependently typed programs have bounded recursion and can be proven to halt. It may be possible to model commutative scripts that are 100% dependently typed, but this by no means can open (to composition and open) the block chain state to every script that someone wants to create.

If Vitalik even had a clue about Computer Science, the first thing he would have done is model the scripting in a purely dependently typed language such as Epigram or Coq.

I must admit I hadn't really expended more than 5 minutes (cumulatively) thinking about it until today.

Edit: this blog post explains a bit about the insoluble synchrony problem. And not surprisingly he uses the same terminology as I did above.