10 ms·

Simplicity: A New Language for Blockchains [pdf]

300 points by TD-Linux 9y ago

maxxxxx 9y ago
For the German speakers: Omega Tau has a pretty good podcast about Ethereum and Solidity: http://omegataupodcast.net/265-ethereum-and-solidity/ http://omegataupodcast.net/265-ethereum-and-solidity/
- icahnvalyou 9y ago
  Is there an English equiv?
- kobeya 9y ago
  What does that have to do with Simplicity?
  - maxxxxx 9y ago
    Nothing :-( . I confused Solidity with Simplicity. Seems I was a little too excited reading "language" and "blockchain". Still a good podcast though.
adamnemecek 9y ago
This field is a killer app of coq. Nowhere else do your bugs cost more while the program size is small.
- DennisP 9y ago
  Someone at the Ethereum Foundation is working full-time on formal verification, and building a smart contract language to make it easier: https://medium.com/@pirapira/bamboo-compiler-started-producing-evm-bytecode-6a55e4633de9 https://medium.com/@pirapira/bamboo-compiler-started-produci... "Currently I’m confident I can write an interpreter of Bamboo in Coq or Isabelle/HOL. I don’t want to expand the language much further until I write one so that I can prove properties of Bamboo programs. Ultimately I’d like to replace the compiler with a proven-correct one, but for that, a Bamboo interpreter needs to exist in a theorem prover."
  - adamnemecek 9y ago
    I'm pumped cause this will popularize theorem provers and pump a lot of money into their development. There was that Stephan Diehl talk on the front page yesterday https://news.ycombinator.com/item?id=15582429 https://news.ycombinator.com/item?id=15582429 where he concluded that it's gonna be a while before see a language based on homotopy type theory. He made a good argument. But these developments make me question whether crypto wont make them popular. This "early future" is kinda amazing.
    - hiker 9y ago
      Cubical https://github.com/mortberg/cubicaltt https://github.com/mortberg/cubicaltt is a proof of concept programming language based on constructive (cubical type theory https://arxiv.org/abs/1611.02108 https://arxiv.org/abs/1611.02108) interpretation of HoTT. Agda also added recently support for cubical paths https://agda.readthedocs.io/en/latest/language/cubical.html https://agda.readthedocs.io/en/latest/language/cubical.html . I'm also waiting on Lean https://leanprover.github.io https://leanprover.github.io to introduce cubical type theory for HoTT. Version 2 of the language had HoTT based on the univalence axiom which was dropped in version 3. With cubical type theory the univalence axiom can be constructively proved and is no longer an axiom.
- nickpsecurity 9y ago
  It would take a lot of talent and time to use. It's why I usually push Design-by-Contract and/or runtime checks/tests. Far as new languages, you might find Noether interesting in how it is built in layers that let one trade verification difficulty vs expressiveness as desired. https://github.com/noether-lang/noether/tree/master/doc/presentations https://github.com/noether-lang/noether/tree/master/doc/pres... Among other interesting features. I recommend reading old one then new one.
  - adamnemecek 9y ago
    I would imagine an idris derivative isnt all that much easier to write when compared with writing coq.
    - nickpsecurity 9y ago
      Oh yeah, Ive known people who could do model checking giving up on Idris since it was too difficult. What's interesting about Noether is it builds up from simplest models of computation to single threaded to distributed. The lower levels are like state machines. One could do that in languages for contracts working up from brute-forceable automata toward more expressive stuff that takes more work. Plus, I thought you'd enjoy the language presentation as extra benefit.
      - willtim 9y ago
        Are we not confusing difficulty with familiarity? For me personally, as someone very familiar with FP, Idris was very approachable and easy to at least write simple proofs in.
      - unboxed_type 9y ago
        I have nothing to say about the language (I gave up reading those cumbersome slides), but I am really amazed that you expect someone to like that presentation! :)
    - mietek 9y ago
      Proving theorems in Agda or Idris is like programming in more rigorous variant of Haskell. Proving theorems in Coq is... different.
- unboxed_type 9y ago
  It is hard to imagine that a proof-assistant will be used as a tool for checking smart-contract correctness due to a lack of sufficiently trained personal. What this BC community is really need is a suitable programming language which will be tailored for functional correctness and expressiveness. Unfortunately, the Simplicity language addresses only the first half, and it is not sufficient for practical success IMO.
udfalkso 9y ago
FYI for the authors. Typo on page 3: " All Bitcoin Script operations are pure functions of the machine state expect for the signature-verification operations. " And page 4: "As such, we expect it to be a target for other, higher-level, languages to be complied to."
- tbodt 9y ago
  They should have formally verified the paper as well as the language.
  - amingilani 9y ago
    Or, if you're lazy like me, get a subscription to grammarly.com. As a technical publications editor I can say that it's worth every penny.
    - jcahill 9y ago
      > Or, if you're a technical publications editor, get a subscription to Grammarly⁽¹⁾. [ed: you almost certainly will not achieve a net benefit from paying a subscription to an orthographic linter.] ____________________ ¹ https://grammarly.com https://grammarly.com
      - amingilani 9y ago
        There's a free tier too but it's definitely great for me! Where I work, we have a policy about using perfect English in every message we send.
johnbender 9y ago
A few thoughts/questions if the authors stop by since I can't seem to find a link to the Coq source: I'm curious if there is an interpreter written in Gallina that implements the semantics? Maybe with a simulation proof (or similar)? It would be pretty sweet to have a verified interpreter. Also, found this in the corresponding blog post while search for the Coq source. > It is Turing incomplete, disallowing unbounded loops and allowing for static analysis It's definitely possible (and not so hard depending) to do proofs and static analysis of looping programs provided the specification can be encoded as an invariant. To be fair I'm not sure what the implications of non-terminating programs are in this setting and with respect to a specification.
- jmgrosen 9y ago
  > I'm curious if there is an interpreter written in Gallina that implements the semantics? Assuming you only want the core language, the semantics is an interpreter -- available in Appendix A.
  - johnbender 9y ago
    I want a Gallina implementation of an interpreter that I can extract to OCaml using Coq. UPDATE: found it thank you.
- netsec_burn 9y ago
  Stupid question, isn't this the Halting Problem?
  - johnbender 9y ago
    Not a stupid question at all! An invariant that is true of all loop iterations is true of all loop iterations even if the loop diverges. Again, I'm not sure what the implications are for divergence in this setting but it doesn't prevent one from proving loop invariants.
    - schoen 9y ago
Frogolocalypse 9y ago
The Reddit post also has some good discussion on it : https://www.reddit.com/r/Bitcoin/comments/79ohjw/bitcoindev_simplicity_an_alternative_to_script/ https://www.reddit.com/r/Bitcoin/comments/79ohjw/bitcoindev_...
tbodt 9y ago
Blockchain programming is fundamentally different from all other programming, and we need a new language to handle that. "Solidity" is far from solid.
- kobeya 9y ago
  This is fundamentally different from Solidity.
  - tbodt 9y ago
    Which is what makes it better.
- unboxed_type 9y ago
  It is far from solid and yet it is easy to understand (modulo corner cases) . I doubt that lambda-calculus-like language will take over it just because it gives one an ability to prove correctness properties in Coq.
thinkloop 9y ago
The biggest difference from Ethereum is not the lack of Turing Completeness but: > Maintain Bitcoin’s design of self-contained transactions whereby programs do not have access to any information outside the transaction. This drastically changes the use cases, and may keep both chains complimentary.
- nullc 9y ago
  > This drastically changes the use cases, I don't agree. It is possible to keep the interaction pure without any practical loss of functionality-- a transaction still has access to its own casual state, in particular using a technique we call covenants (which is mentioned in the paper). This kind of controlled state management avoids the destruction of scalablity (no caching, no parallelism, no out of order processing, no skipping activity when overloaded) that we've seen in other systems. Using covenants Russel was, in earlier work, able to implement "Vaults"-- a kind of useful smart contract some have described as impossible in Bitcoin-- in the elements implementation of Bitcoin Script (it uses opcodes that are currently disabled in Bitcoin) with no changes to any of the system's state management. Part of the overall intent with Simplicity is to make this kind of approach efficient and accessible.
tw1010 9y ago
What I love about all this is that it is almost entirely developed by the community, without any central authority preventing it from going in any particular direction. (There might be powerful players incentivizing certain branches, but that has limited effect for a thing like this.) So despite what critics say (and I admit to agreeing with them on some points), it just feels like this whole thing has such a momentum and enthusiasm behind it that something really cool will come out of it within 5-10 years, no matter what problems people point out about it at the moment.
- nosuchthing 9y ago
  Wait what? Blockstream's business model depends on selling services to enterprises, that's why they keep attempting to prevent upgrades to the blocksize, to the detriment of high fees and a clogged network. The paper here is written by a single member employed by Blockstream.
  - Frogolocalypse 9y ago
    bitmain blocked the blocksize increase of segwit for almost a year. Take it up with them.
  - grubles 9y ago
    The block size limit has been increased for a number of months now, which was supported by everyone at Blockstream AFAIK. >to the detriment of high fees and a clogged network. Sigh. It is astonishingly cheap to spend bitcoin right now. In fact, I paid the absolute minimum fee (1000 satoshis, or a handful of cents) the other day.
    - nsomaru 9y ago
      How long did your payment take to clear?
      - once_inc 9y ago
        Mine was 5 sat/byte. 3 conf in 30min.
domainkiller 9y ago
doesn't feel simple :|
- fnordsensei 9y ago
  It might refer to the objective "simple" as opposed to "complex", rather than the subjective "easy" (as opposed to "hard").
sciyoshi 9y ago
Looks exciting - will need to take some time to read this in more detail. Off-hand, will this not be able to handle ASN.1 certificates due to their Turing completeness?
- TD-Linux 9y ago
  I don't know if ASN.1 is turing complete, but I don't think Simplicity can handle arbitrary depth recursion, either. Luckily, to parse a BER coded certificate, you only need a fixed depth. Of course, if you are actually parsing BER in a smart contract, you should really reconsider what life choices brought you to this point :) But it might be useful for a non-blockchain related crypto library.
- nullc 9y ago
  You can express reading ASN.1 certificates in Simplicity so long as you have an additional explicit constraint on their depth. In practice one always exists, just not explicitly, and instead implementations will randomly fail or disagree with each other where you exceed their hidden limits... limits which might arise out of their construction implicitly (and depend on the user's configuration) and not even be known to the program authors.
pankajdoharey 9y ago
After reading the paper you will see why Simplicity is not the right language for this semantics. Lisps are better fit for such tasks.
- 4lch3m1st 9y ago
  I will need to take a more careful look, mostly because it was too complex for my understanding, but some of the code indeed look a little like Lisp. EDIT: Why do you say that?
deleted 9y ago
[deleted]
runeks 9y ago
This looks really interesting! I think purity is a perfect fit for smart contracts, since there’s no global state to access — at least in the Bitcoin blockchain — and side effects don’t make much sense. Question: speaking in Haskell-terms, is this Simplicity Core language similar to GHC Core in that it’s a typed intermediate language (not intended to be written by programmers)? Would be nice to see a higher-level language that compiles to, first, Simplicity Core and then Bitcoin script — including example contracts implemented in that language (ie. the various contracts used for Lighting Network).
unboxed_type 9y ago
I do appreciate the author's attempt to create a new worthy language really, I do a research on this topic myself. What concerns me is that the presented language is not suitable for any practical programming. Even for the most simple smart contracts, the final Simplicity program will be huge and unreadable due to the lack of familiar data structures and constructs. The language resembles me some kind of lambda calculus which is good for theoretical investigation, but not suitable for practical stuff. I am not ready to exchange a language convenience for better provability: it must have both issues addressed at the same time, only then the mix will be right for an end-user.
- cousin_it 9y ago
  Yeah. It seems equivalent in power to combinatorial logic, which is weaker than finite state machines, which are weaker than Turing machines. In fact I don't even understand why a blockchain language must emphasize provability. Why not use something like LLVM IR and let compilers handle verification?
  - unboxed_type 9y ago
    >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.
    - cousin_it 9y ago
      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.

300 points by TD-Linux 9y ago

For the German speakers: Omega Tau has a pretty good podcast about Ethereum and Solidity: http://omegataupodcast.net/265-ethereum-and-solidity/ http://omegataupodcast.net/265-ethereum-and-solidity/

icahnvalyou 9y ago
Is there an English equiv?
kobeya 9y ago
What does that have to do with Simplicity?
- maxxxxx 9y ago
  Nothing :-( . I confused Solidity with Simplicity. Seems I was a little too excited reading "language" and "blockchain". Still a good podcast though.

adamnemecek 9y ago

This field is a killer app of coq. Nowhere else do your bugs cost more while the program size is small.

DennisP 9y ago
Someone at the Ethereum Foundation is working full-time on formal verification, and building a smart contract language to make it easier: https://medium.com/@pirapira/bamboo-compiler-started-producing-evm-bytecode-6a55e4633de9 https://medium.com/@pirapira/bamboo-compiler-started-produci... "Currently I’m confident I can write an interpreter of Bamboo in Coq or Isabelle/HOL. I don’t want to expand the language much further until I write one so that I can prove properties of Bamboo programs. Ultimately I’d like to replace the compiler with a proven-correct one, but for that, a Bamboo interpreter needs to exist in a theorem prover."
- adamnemecek 9y ago
  I'm pumped cause this will popularize theorem provers and pump a lot of money into their development. There was that Stephan Diehl talk on the front page yesterday https://news.ycombinator.com/item?id=15582429 https://news.ycombinator.com/item?id=15582429 where he concluded that it's gonna be a while before see a language based on homotopy type theory. He made a good argument. But these developments make me question whether crypto wont make them popular. This "early future" is kinda amazing.
  - hiker 9y ago
    Cubical https://github.com/mortberg/cubicaltt https://github.com/mortberg/cubicaltt is a proof of concept programming language based on constructive (cubical type theory https://arxiv.org/abs/1611.02108 https://arxiv.org/abs/1611.02108) interpretation of HoTT. Agda also added recently support for cubical paths https://agda.readthedocs.io/en/latest/language/cubical.html https://agda.readthedocs.io/en/latest/language/cubical.html . I'm also waiting on Lean https://leanprover.github.io https://leanprover.github.io to introduce cubical type theory for HoTT. Version 2 of the language had HoTT based on the univalence axiom which was dropped in version 3. With cubical type theory the univalence axiom can be constructively proved and is no longer an axiom.
nickpsecurity 9y ago
It would take a lot of talent and time to use. It's why I usually push Design-by-Contract and/or runtime checks/tests. Far as new languages, you might find Noether interesting in how it is built in layers that let one trade verification difficulty vs expressiveness as desired. https://github.com/noether-lang/noether/tree/master/doc/presentations https://github.com/noether-lang/noether/tree/master/doc/pres... Among other interesting features. I recommend reading old one then new one.
- adamnemecek 9y ago
  I would imagine an idris derivative isnt all that much easier to write when compared with writing coq.
  - nickpsecurity 9y ago
    Oh yeah, Ive known people who could do model checking giving up on Idris since it was too difficult. What's interesting about Noether is it builds up from simplest models of computation to single threaded to distributed. The lower levels are like state machines. One could do that in languages for contracts working up from brute-forceable automata toward more expressive stuff that takes more work. Plus, I thought you'd enjoy the language presentation as extra benefit.
    - willtim 9y ago
      Are we not confusing difficulty with familiarity? For me personally, as someone very familiar with FP, Idris was very approachable and easy to at least write simple proofs in.
    - unboxed_type 9y ago
      I have nothing to say about the language (I gave up reading those cumbersome slides), but I am really amazed that you expect someone to like that presentation! :)
  - mietek 9y ago
    Proving theorems in Agda or Idris is like programming in more rigorous variant of Haskell. Proving theorems in Coq is... different.
unboxed_type 9y ago
It is hard to imagine that a proof-assistant will be used as a tool for checking smart-contract correctness due to a lack of sufficiently trained personal. What this BC community is really need is a suitable programming language which will be tailored for functional correctness and expressiveness. Unfortunately, the Simplicity language addresses only the first half, and it is not sufficient for practical success IMO.

udfalkso 9y ago

FYI for the authors. Typo on page 3: " All Bitcoin Script operations are pure functions of the machine state expect for the signature-verification operations. " And page 4: "As such, we expect it to be a target for other, higher-level, languages to be complied to."

tbodt 9y ago
They should have formally verified the paper as well as the language.
- amingilani 9y ago
  Or, if you're lazy like me, get a subscription to grammarly.com. As a technical publications editor I can say that it's worth every penny.
  - jcahill 9y ago
    > Or, if you're a technical publications editor, get a subscription to Grammarly⁽¹⁾. [ed: you almost certainly will not achieve a net benefit from paying a subscription to an orthographic linter.] ____________________ ¹ https://grammarly.com https://grammarly.com
    - amingilani 9y ago
      There's a free tier too but it's definitely great for me! Where I work, we have a policy about using perfect English in every message we send.

johnbender 9y ago

A few thoughts/questions if the authors stop by since I can't seem to find a link to the Coq source: I'm curious if there is an interpreter written in Gallina that implements the semantics? Maybe with a simulation proof (or similar)? It would be pretty sweet to have a verified interpreter. Also, found this in the corresponding blog post while search for the Coq source. > It is Turing incomplete, disallowing unbounded loops and allowing for static analysis It's definitely possible (and not so hard depending) to do proofs and static analysis of looping programs provided the specification can be encoded as an invariant. To be fair I'm not sure what the implications of non-terminating programs are in this setting and with respect to a specification.

jmgrosen 9y ago
> I'm curious if there is an interpreter written in Gallina that implements the semantics? Assuming you only want the core language, the semantics is an interpreter -- available in Appendix A.
- johnbender 9y ago
  I want a Gallina implementation of an interpreter that I can extract to OCaml using Coq. UPDATE: found it thank you.
netsec_burn 9y ago
Stupid question, isn't this the Halting Problem?
- johnbender 9y ago
  Not a stupid question at all! An invariant that is true of all loop iterations is true of all loop iterations even if the loop diverges. Again, I'm not sure what the implications are for divergence in this setting but it doesn't prevent one from proving loop invariants.
  - schoen 9y ago

Frogolocalypse 9y ago

The Reddit post also has some good discussion on it : https://www.reddit.com/r/Bitcoin/comments/79ohjw/bitcoindev_simplicity_an_alternative_to_script/ https://www.reddit.com/r/Bitcoin/comments/79ohjw/bitcoindev_...

tbodt 9y ago

Blockchain programming is fundamentally different from all other programming, and we need a new language to handle that. "Solidity" is far from solid.

kobeya 9y ago
This is fundamentally different from Solidity.
- tbodt 9y ago
  Which is what makes it better.
unboxed_type 9y ago
It is far from solid and yet it is easy to understand (modulo corner cases) . I doubt that lambda-calculus-like language will take over it just because it gives one an ability to prove correctness properties in Coq.

thinkloop 9y ago

The biggest difference from Ethereum is not the lack of Turing Completeness but: > Maintain Bitcoin’s design of self-contained transactions whereby programs do not have access to any information outside the transaction. This drastically changes the use cases, and may keep both chains complimentary.

nullc 9y ago
> This drastically changes the use cases, I don't agree. It is possible to keep the interaction pure without any practical loss of functionality-- a transaction still has access to its own casual state, in particular using a technique we call covenants (which is mentioned in the paper). This kind of controlled state management avoids the destruction of scalablity (no caching, no parallelism, no out of order processing, no skipping activity when overloaded) that we've seen in other systems. Using covenants Russel was, in earlier work, able to implement "Vaults"-- a kind of useful smart contract some have described as impossible in Bitcoin-- in the elements implementation of Bitcoin Script (it uses opcodes that are currently disabled in Bitcoin) with no changes to any of the system's state management. Part of the overall intent with Simplicity is to make this kind of approach efficient and accessible.

tw1010 9y ago

What I love about all this is that it is almost entirely developed by the community, without any central authority preventing it from going in any particular direction. (There might be powerful players incentivizing certain branches, but that has limited effect for a thing like this.) So despite what critics say (and I admit to agreeing with them on some points), it just feels like this whole thing has such a momentum and enthusiasm behind it that something really cool will come out of it within 5-10 years, no matter what problems people point out about it at the moment.

nosuchthing 9y ago
Wait what? Blockstream's business model depends on selling services to enterprises, that's why they keep attempting to prevent upgrades to the blocksize, to the detriment of high fees and a clogged network. The paper here is written by a single member employed by Blockstream.
- Frogolocalypse 9y ago
  bitmain blocked the blocksize increase of segwit for almost a year. Take it up with them.
- grubles 9y ago
  The block size limit has been increased for a number of months now, which was supported by everyone at Blockstream AFAIK. >to the detriment of high fees and a clogged network. Sigh. It is astonishingly cheap to spend bitcoin right now. In fact, I paid the absolute minimum fee (1000 satoshis, or a handful of cents) the other day.
  - nsomaru 9y ago
    How long did your payment take to clear?
    - once_inc 9y ago
      Mine was 5 sat/byte. 3 conf in 30min.

domainkiller 9y ago

doesn't feel simple :|

fnordsensei 9y ago
It might refer to the objective "simple" as opposed to "complex", rather than the subjective "easy" (as opposed to "hard").

sciyoshi 9y ago

Looks exciting - will need to take some time to read this in more detail. Off-hand, will this not be able to handle ASN.1 certificates due to their Turing completeness?

TD-Linux 9y ago
I don't know if ASN.1 is turing complete, but I don't think Simplicity can handle arbitrary depth recursion, either. Luckily, to parse a BER coded certificate, you only need a fixed depth. Of course, if you are actually parsing BER in a smart contract, you should really reconsider what life choices brought you to this point :) But it might be useful for a non-blockchain related crypto library.
nullc 9y ago
You can express reading ASN.1 certificates in Simplicity so long as you have an additional explicit constraint on their depth. In practice one always exists, just not explicitly, and instead implementations will randomly fail or disagree with each other where you exceed their hidden limits... limits which might arise out of their construction implicitly (and depend on the user's configuration) and not even be known to the program authors.

pankajdoharey 9y ago

After reading the paper you will see why Simplicity is not the right language for this semantics. Lisps are better fit for such tasks.

4lch3m1st 9y ago
I will need to take a more careful look, mostly because it was too complex for my understanding, but some of the code indeed look a little like Lisp. EDIT: Why do you say that?

deleted 9y ago

[deleted]

runeks 9y ago

This looks really interesting! I think purity is a perfect fit for smart contracts, since there’s no global state to access — at least in the Bitcoin blockchain — and side effects don’t make much sense. Question: speaking in Haskell-terms, is this Simplicity Core language similar to GHC Core in that it’s a typed intermediate language (not intended to be written by programmers)? Would be nice to see a higher-level language that compiles to, first, Simplicity Core and then Bitcoin script — including example contracts implemented in that language (ie. the various contracts used for Lighting Network).

unboxed_type 9y ago

I do appreciate the author's attempt to create a new worthy language really, I do a research on this topic myself. What concerns me is that the presented language is not suitable for any practical programming. Even for the most simple smart contracts, the final Simplicity program will be huge and unreadable due to the lack of familiar data structures and constructs. The language resembles me some kind of lambda calculus which is good for theoretical investigation, but not suitable for practical stuff. I am not ready to exchange a language convenience for better provability: it must have both issues addressed at the same time, only then the mix will be right for an end-user.

cousin_it 9y ago
Yeah. It seems equivalent in power to combinatorial logic, which is weaker than finite state machines, which are weaker than Turing machines. In fact I don't even understand why a blockchain language must emphasize provability. Why not use something like LLVM IR and let compilers handle verification?
- unboxed_type 9y ago
  >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.
  - cousin_it 9y ago
    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.