GOPHERSPACE.DE - P H O X Y
gophering on hngopher.com
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?.