HN Gopher Feed (2017-10-30) - page 1 of 10 ___________________________________________________________________
Simplicity: A New Language for Blockchains [pdf]
126 points by TD-Linux
https://blockstream.com/simplicity.pdf___________________________________________________________________
tbodt - 1 hours 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 - 21 minutes ago
This is fundamentally different from Solidity.
thinkloop - 1 hours 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.
tw1010 - 34 minutes 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.
domainkiller - 30 minutes ago
doesn't feel simple :|
Frogolocalypse - 2 hours ago
The Reddit post also has some good discussion on it
:https://www.reddit.com/r/Bitcoin/comments/79ohjw/bitcoindev_...
adamnemecek - 2 hours ago
This field is a killer app of coq. Nowhere else do your bugs cost
more while the program size is small.
nickpsecurity - 9 minutes 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/pres...Among other interesting
features. I recommend reading old one then new one.
adamnemecek - 5 minutes ago
I would imagine an idris derivative isnt all that much easier
to write when compared with writing coq.
DennisP - 1 hours 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-
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 - 1 hours 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 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.
maxxxxx - 1 hours ago
For the German speakers: Omega Tau has a pretty good podcast about
Ethereum and Solidity: http://omegataupodcast.net/265-ethereum-
and-solidity/
kobeya - 16 minutes ago
What does that have to do with Simplicity?
icahnvalyou - 39 minutes ago
Is there an English equiv?
udfalkso - 2 hours 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 - 1 hours ago
They should have formally verified the paper as well as the
language.
amingilani - 18 minutes 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.
johnbender - 1 hours 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
analysisIt'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.
kobeya - 17 minutes ago
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.
jmgrosen - 1 hours 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 - 1 hours ago
I want a Gallina implementation of an interpreter that I can
extract to OCaml using Coq.UPDATE: found it thank you.
netsec_burn - 1 hours ago
Stupid question, isn't this the Halting Problem?
johnbender - 59 minutes 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 - 35 minutes ago
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".
kobeya - 16 minutes ago
The important word there was ?every?.