Simplicity: A New Language for Blockchains [pdf]
blockstream.com
blockstream.com
"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."
He made a good argument. But these developments make me question whether crypto wont make them popular. This "early future" is kinda amazing.
Agda also added recently support for cubical paths https://agda.readthedocs.io/en/latest/language/cubical.html .
I'm also waiting on Lean 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.
https://github.com/noether-lang/noether/tree/master/doc/pres...
Among other interesting features. I recommend reading old one then new one.
Plus, I thought you'd enjoy the language presentation as extra benefit.
I do proofs and write small programs in coq regularly. I've spent most of my professional life as a web developer.
As with everything learning to do proofs and learning to use Coq are a matter of time, effort, and access to good documentation and other resources.
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.
>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.
Yep, that's what happens when demand decreases for a good or service.
Someone put it very well the other day when they said "The only winners in the scaling debate has been alt coins"
Also it's quiet interesting that every major price increase, and nose dive has been associated with multi-million dollar margin trading on Bitfinix via Tether markets (which are suspected to be created out of thin air).
If the allegations are true, Bitcoin's price is mostly the result of a market controlled by a single exchange, who now holds a significant percentage of the supply.
The Bitfinex conspiracy is fun and entertaining to read about but more likely than not the guy probably sold early and is trying to affect the markets with FUD.
The unregulated exchanges are able to act in fractional reserve as they're not required to audit their deposits. The exchanges are also able, and have been wash trading, front running, and spoofing orders, creating a false sense of volume and activity.
https://i.imgur.com/ZwQ63OE.png
Transaction volume took a cliff dive once Chinese regulators forced exchanges to charge per transaction.
Bitcoins are produced for a nominal value, it's not magic or limited in supply, it's reproducible software. The same service is offered by many other blockchain networks.
2 out of the top 10 committers work for Blockstream (matt works at Chaincode Labs now).
Care to revisit your conspiracy? Or is something wrong with the data?
Garzik, Hearn, Andresen. Gone.
The extent of Hearn's involvement in the project was a couple commits in 2013 and 2014. Gavin-- once a fairly active and appreciated contributor-- sunsetted himself years before, primarily to focus on creating the "Bitcoin Foundation" though he later alienated himself completely after the foundation discredited itself and largely imploded with rather abusive public attacks ("should be fired") and by vigorously backing a pretty obvious scammer. But in spite the bad blood there, you don't see support for your conspiracy theories -- because there really just isn't any substance to them.
If you look at active project competition most of the same people who are most active today have been most active pretty much all along:
/-----------------------------------------------------------------------------
| Non-merge commits in Bitcoin project git
| 2010 2011 2012 2013 2014 2015 2016 2017 All | Active months
|-----------------------------------------------------------------------------
|Wladimir 1 349 159 115 384 193 197 93 1491 | 73
|Pieter 0 51 227 111 170 89 156 112 916 | 75
|Matt 0 101 71 38 25 54 100 143 532 | 66
|Gavin 17 152 139 112 47 17 1 2 487 | 61
|Garzik 0 38 106 35 48 7 0 0 234 | 36
|Hearn 0 0 1 7 2 1 0 0 11 | 8
...That's said, Gavin was driven out of Bitcoin development at the time by you and your team blocking any block size increase with dumb arguments. The interested reader will search bitcointalk for such recurring discussion. He then created Bitcoin XT wich included a voting system for miners to vote for bigger blocks. XT nodes were the target of massive Ddos attacks, and some miners were as well. XT failed because of that, despite a growing support for big blocks. From that day Gavin and Mike gave up knowing that small blockers had taken control of Bitcoin, thanks to the $70'000'000 AXA and other investors put into Blockstream.
The whole Bitcoin foundation was a side project of him, and did not discredit itself. But since /r/bitcoin and bitcointalk was already controlled by people supporting small blocks, and very complaisant with Blockstream, you and Luke Jr and others used those channels to spread misinformation about this foundation run by people supporting big blocks. Today, such discussions channels are so censored that only remains (probably paid) trolls, small blockers and newcomers completely lost in this shitshow. Banned people created /r/btc and this sub is growing quite fast and sometime has more active users than /r/bitcoin does.
Fun fact about you: you used the same kind of practice when you were contributing to Wikipedia. Indeed, you were aggressively blanking user page because of supposed copyright violation no one but you cared about. After dozens of complaints you received a ban but in the meantime you automated the process using a sock puppet account. Hopefully at the end they got you out, the "toxic" and "insane" "gmaxwell".
Last but not least, comparing commit number does not highlight the role of each individual. Gavin was a project leader and could see the big picture. It's like saying Linus Torvalds is useless because he barely does non-merge commit. Gavin saw the small block shitshow coming from miles away, he saw the fee rising from miles away. Bitcoin is in a very poor state, blocks are full, the fee market makes no sense ans is quite unstable, sides chains were proven impractical to reach VISA level of transactions, and LN is no more than a take over of banks on Bitcoin. We are talking of fees bigger than a dollar for a classic transaction, already micro transactions are not possible anymore with Bitcoin. No wonders why Ethereum is taking the lead.
Anyway I will stop here, it's a pain to write comments on mobile phones. If this interests you, have a look to the sticky post in /r/btc, it contains sourced and well written links about the current Bitcoin situation and how we got there.
>Banned people created /r/btc and this sub is growing quite fast
No, Roger Ver uses that subreddit to advertise his commercial website - breaking reddit.com's terms of service.
Also, Ethereum is in a quagmire regarding scaling. In fact, I do believe it's cheaper to spend bitcoin now than it is ether ($0.25 in gas per transaction).
"Quagmire" is a bit provocative, but yes scaling is a serious problem that needs to be solved.
> In fact, I do believe it's cheaper to spend bitcoin now than it is ether ($0.25 in gas per transaction).
This is no longer true. Since the recent fork/upgrade, it's been consistently cheap. Specifically, an ether transfer with an $0.001 fee rarely takes more than a few minutes to confirm.
A good indication you don't have valid criticism is when your reasoning falls back to the reddit terms of service.
In r/btc, if you happen to have an opposing opinion you will be scolded, insulted, and more than likely put on some targeted harassment list [0].
[0] https://np.reddit.com/r/TWHB/comments/7627ok/mass_troll_list...
Stop the Orwellian doublespeak There is a one-line constant that changes block-size.
Segwit was a giant change that's a one-trick pony that core wanted for their own reasons. It hasn't been effective at reducing the backlog, and segwit transaction percentage is declining.
Your doublespeak won't work here because no one censors comments that disagree.
Also, it's pretty interesting how you completely avoid talking about the targeted harassment list of Core supporters I posted in my previous comment.
I don't think it is interesting at all. I have no idea what the subreddit you linked to r/TWHB is? In terms of the censorship, I have seen it first hand on my own comments and it irritated me, so that's why I complain about it. No idea about your whataboutism example, though.
Instead of loudly denouncing it, youre smug about it. You're the very thing Bitcoin was made to destroy and you should be ashamed of your actions.
It's a subreddit. Subreddits are moderated. Stop misusing the word "censorship". Calling moderation of a subreddit "censorship" flies in the face of those actually affected by the suppression of information by their governments.
Hearn: https://blog.plan99.net/the-resolution-of-the-bitcoin-experi...
Andresen: https://cointelegraph.com/news/andresen-proposes-block-incre...
Garzik: https://www.cryptocoinsnews.com/bitcoin-core-dev-jeff-garzik...
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.
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.
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.
Approaches like your (2) are unfortunately fraught with easy vulnerabilities.
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.
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.
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.
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.
[1] https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2017...
When a suitably rich set of jets is available, we expect the bulk of the
computation specified by a Simplicity program to be made up of these jets,
with only a few combinators used to combine the various jets. This should
bring the computational requirements needed for Simplicity programs in line
with existing blockchain languages. In light of this, one could consider Simplicity
to be a family of languages, where each language is defined by a set of jets that
provide computational elements tailored for its particular application.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.
Assuming you only want the core language, the semantics is an interpreter -- available in Appendix A.
UPDATE: found it thank you.
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.
An example I like to use is that many people seem to believe that there is no reason to use anything other than the obvious greedy approximation algorithm for the minimal set cover problem because of a celebrated result in approximation theory that shows that no algorithm can achieve a better worst case approximation gap. Last I checked, the Wikipedia article-- for example-- pushes people in that direction.
It turns out in practice, however, on many problem cases the obvious greedy algorithm is pretty bad and simple heuristics on top of it do a LOT better. People are mistaking worst case with "average" or "typical" case.
In the problem space we're discussing here with Simplicity though, there are cases where undecidable isn't really an option: For example, if the consensus rules of a system impose execution cost limits, the result of evaluating the costs can't permit "undecidable", and so it's arguably better to work from a framework which guarantees that it won't be by construction... rather than attempting a game-of-operation where minor modifications to your program might seemingly randomly knock into undecidable-land.
I presume that a programming language is a compromise between expressiveness and decidability. Cost estimation feature is definitely a good one until having that feature stops you from being able to develop your business logic in a convenient-enough manner. Regarding the latter, I am not convinced that Simplicity is a nice fit.
Simplicity is explicitly not Turing-complete: it is not possible to write a Simplicity program that loops forever. In other words, Simplicity is a total functional programming language: every Simplicity program will finish computing in a finite number of steps.
See Turner 2004 for a great introduction to total functional programming: https://github.com/mietek/total-functional-programming/blob/...
Totality is also important in the context of theorem-proving: if we're interested in treating programs as proofs, and types as propositions, then the type system of our language must correspond to a consistent logic. Otherwise, if we could write a program that loops forever, we could prove any proposition, and so our logic would be inconsistent. Languages such as Agda, Coq, and Idris are total, and writing programs in them is constructive theorem-proving.
Wadler 2015 places the above principle in a fascinating historical context: http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-...
[1]: Some argue that Turing-completeness is not a property of languages, but rather of their runtime semantics. McBride 2015 has more details: https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b8...
Note that you can do things like unroll a loop entirely and build a Merkle tree of the possible unrolled versions, just revealing at redemption time the one actually used.
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).
> 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.
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.
And page 4: "As such, we expect it to be a target for other, higher-level, languages to be complied to."
[ed: you almost certainly will not achieve a net benefit from paying a subscription to an orthographic linter.]
____________________
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.
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.
https://www.reddit.com/r/Bitcoin/comments/79ohjw/bitcoindev_...
EDIT: Why do you say that?