"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."
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 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.
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.
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.
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.
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.
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! :)
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.
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.
This statement confuses me since Blockstream has positioned itself to be the central authority. They seem to be attempting to remove power from users, businesses, and miners in order to centralize and consolidate power so they are the only people who make decisions regarding Bitcoin. Effectively, a company that's only been around for a few years has been attempting to put itself into a monopoly controlling position of a 100-billion dollar commodity.
They've managed to kick or drive out anyone who has disagreed, so yeah, the sheep that are left are not problematic and produce only the appropriate agreeable noises.
This is simply untrue, and not a claim that even any of those people have had the audacity to make.
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:
Just chance that the big-block folks happen to be gone? Nice table, but LoC is way different (and less important) than being the person deciding what gets merged. Show me the merge commits table.
I don't know how you're able to look yourself in the mirror every day. You joined a project that promoted freedom of speech and liberty. Now you endorse and benefit from the disgusting censorship taking place on /r/bitcoin and the bitcointalk forum. Its censorship on a scale suitable for the history books.
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.
>Its censorship on a scale suitable for the history books.
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.
Just for the reader awareness: this guy right here in Gregory Maxwell, a key person working for Blockstream. Nullc actively support 1Mb block to artificially cripple the blockchain and thus create artificial demand for their centralized and bank-like product: side chains and LN hubs.
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.
It's always interesting seeing the conspiracy theorists emerge on Hackernews, of all places. Gavin himself stated he should have removed his own commit access due to inactivity. Of course, it was removed for him due to being social engineered by Craig Wright (the fake Satoshi guy evading taxes).
>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).
> Also, Ethereum is in a quagmire regarding scaling.
"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.
Try posting in r/bitcoin favoring larger blocks. Be as logical as you want. Try disagreeing with anything about the fee market, or saying something critical about core's approach. See if your comment disappears. Hint: it usually will. You might get downvoted, but in /btc you can say what you want. I have trouble believing that leaders that rely on censorship are good stewards for censhorship resistant currency.
A good indication you don't have valid criticism is when your reasoning falls back to the reddit terms of service.
> been excited about bigger blocks (Segregated Witness) for nearly two years.
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.
I think you're getting a little out of touch with reality here. It's verifiable, demonstrable, literally happening now that more transaction data is transmitted on the wire than previously.
Also, it's pretty interesting how you completely avoid talking about the targeted harassment list of Core supporters I posted in my previous comment.
> 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.
They sought to promote themselves to the managerial/business roles that no longer required to write much code. That makes them less involved with the development, not the other way around. I don't think the reason for them to start a business is because someone else urges them to stop writing code for bitcoin.
blockstream has incredible influence on Core no matter which way you split your hairs. Greg Maxwell, Luke Dashjr, Adam Back and Andrew Poelstra act as spokespeople for Core in various forums on a daily basis.
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.
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.
Well, hardly anyone is using it for anything other than speculating it might be useful one day. Everyone buys and lets the coins sit and for some reason people think this is a good useful thing to do?
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.
It's perfectly reasonable to simply buy bitcoin and sit on it, if only for the reason it acts as a store of value relative to unstable government currency (eg. Venezuela, Zimbabwe).
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 store of value is a myth, as the value requires buyers on the markets.
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.
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.
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.
One suggested way to use it is to basically make a "jet" for every existing Bitcoin Script [1]. Then you compose a script make exclusively of these jets and it's no worse than Bitcoin Script. Of course, I think that there's probably better solutions than that.
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.
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?
>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.
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.
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.
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.
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.
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.
"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.
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.
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.
The paper seems to address this. It notes that some loop constructs could be made available but it would make the resource consumption estimation unnecessarily conservative.
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.
This is actually a very good question. The halting problem only applies if you can write a program that loops forever. In other words, the halting problem is only a problem in Turing-complete languages [1], or in languages that admit uncontrolled general recursion. (Likewise for Rice's theorem.)
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.
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.
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.
I keep encountering what I think is a misunderstanding of Rice's Theorem. Rice's Theorem says no program can correctly decide any nontrivial property for every program. However, there are programs that can correctly decide nontrivial properties for many programs! To avoid the Rice's Theorem issue, you just need to be able to say "Don't know"/"Couldn't decide".
Right, exactly! The theorem doesn't forbid the possibility of software that decides properties of some programs (including many useful properties for many useful programs).
This frustrates me a lot too-- I view it as an example of a general peeve of mine that people read too much into formal results often in a pretty cult like manner.
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.
> 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.
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).
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.
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."
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?
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.
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.
