[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.