1) one can introduce a human component by having an escrow. That way one can deploy contracts which can be changed at runtime. Correctness is important, but it is always the question to what criterium? A program can be "correct" and still fail. Actually pure notions of correctness are maybe counter productive here. If we would start to see these things use in the real world we would discover quickly that there is an element of modeling here.

Yeah, this "language" is really not going to be useful anywhere. A big company raising many millions of dollars should have tested their academic ideas in the field before releasing sth like this. I'd be far more impressed by some actual use cases.