[unboxed_type]

>In fact I don't even understand why a blockchain language must emphasize provability.

For two reasons:

1) A smart contract can not be changed in a BC after deployment, so it has to be correct up-front (I am not sure if this fact is obvious for readers, so I decided to add it).

2) A compiler is able to deduce only a limited set of properties. Actually, the less expressive language you have, the more properties you can deduce at compile-time.

The proposed language have chosen to be less expressive to get a higher degree of decidability. But, in my opinion, it goes to the extreme where it becomes no longer useful. The real thing would be to find the right intersection of decidability and expressiveness.

[macroexchange]

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.

[unboxed_type]

I can program a contract that can be parameterized with an address of some other sub-contract (then, say, store it in variable), which I call to do some particular logic. If I change that sub-contract address, I can effectively change my contracts logic. Is that what you?

I would like to mention an interesting paper regarding the topic: Marino, Juels - Setting Standards for Altering and Undoing Smart Contracts (2016).

I see your point about 'pure notions of correctness'. While I agree that some interesting properties of a contract is not easy to come up with (and hence verify), I still believe that there are some 'safety' properties which are far easier to articulate.

I also believe that there is an element of modeling: it may be a viable way of validating properties.

[cousin_it]

That doesn't answer my question at all! Which of these sounds better to you:

1) Have Simplicity running on the blockchain

2) Have dumb old JS running on the blockchain, and transpile Simplicity (or anything else) to it using formally verified tools

I think (2) is better in every way. It lets everyone choose their own tradeoff of safety vs convenience, and leaves the door open for future advances in verification instead of locking in Simplicity forever.

[unboxed_type]

Oh, sorry for that, the question was misunderstood.

I presume that a user-level contract language like Simplicity is going to be translated into low-level byte code like EVM. That low-level code is what gets executed on the blockchain. People can choose other languages with less guarantees, write contracts in those languages, and those contracts will be interoperable with each other. This is how things work right now. In my view the real problem is to introduce a language that will be both safe and expressive at the same time.

[naasking]

You're neglecting the vulnerabilities associated with full abstraction failures: http://lambda-the-ultimate.org/node/5364

Approaches like your (2) are unfortunately fraught with easy vulnerabilities.

[cousin_it]

That doesn't seem like an argument against (2). You're just making the reasonable point that linking your code with someone else's unverified code is a bad idea.

[naasking]

"Unverified code" isn't the problem, because a module could do exactly what it's verified to do. The problem is that the underlying execution model exposes capabilities that the high-level language cannot represent. This lets attackers silently violate invariants that your language is supposed to enforce.

For instance, at one point on the CLR you could throw an object of any type, it didn't have to inherit from System.Exception. But the C# compiler required you to inherit from System.Exception, so a properly crafted callback from a "malicious" module could escape the your C# program's control-flow by throwing an exception that you couldn't catch.

There are loads of full abstraction failures in the JVM and other languages. So if your cryptocurrency VM can execute arbitrary programs, but your surface language is a non-Turing complete language, unless you're very, very careful, you're virtually guaranteed to introduce vulnerabilities due to full abstraction failures.

This property is incredibly subtle, so I wouldn't discount it so easily, particularly when there's so much money involved.