Byzantine Fault Tolerant Raft With Smart Contracts

Re:Byzantine Fault Tolerant Raft With Smart Contracts by brighton36 on Wednesday March 02, 2016 @08:13PM (#11214371)

Does this project actually escrow value, via PoW, or is it merely a message passing protocol?

[ Parent | on HN ]

Re:Byzantine Fault Tolerant Raft With Smart Contracts by carterschonwald on Wednesday March 02, 2016 @08:48PM (#11214515)

the hopper language (the version used in this repo is an earlier snapshot of work from this fall that essentially a minimal scheme / lambda calculus with program level transactional memory) provides mechanisms for first class ownership. Current hopper master is under a huge amount of churn towards the full language we're building, so unless you enjoy reading compiler code bases under heavy active dev, the best i can say is this: stay tuned :)

linear logic provides a nice vehicle for modelling first class ownership. namely: holding a value in a program IS owning it. That plus a lot of ideas from languages/tools like Agda, Coq, Lean, and Idris along with some of what i've learned being an occasional contributor to GHC, plus general PL tech, are going into Hopper, though the current code base

[ Parent | on HN ]

Re:Byzantine Fault Tolerant Raft With Smart Contracts by thedatabase on Wednesday March 02, 2016 @11:32PM (#11215044)

Cool project!

Are you using dependent linear types? Or are you using dependent types some places, and non-dependent linear types for the ownership semantics?

[ Parent | on HN ]

Re:Byzantine Fault Tolerant Raft With Smart Contracts by carterschonwald on Thursday March 03, 2016 @07:27AM (#11216397)

Excellent Question. The notion of linearity were starting with for type system design corresponds with runtime linear usage, which Means linear computations that are pure can be lifted into types because they don't have any runtime usage.

One of the More surprising / interesting realizations we had recently was that the copattern matching for coinductive Data as seen in Agda is exactly what's needed to define pattern matching sanely on certain linear type operators like &

Which then let's you very succinctly model problems like having cake vs eating it. The original escrow of deliciousness vs the pretty cake

[ Parent | on HN ]

Re:Byzantine Fault Tolerant Raft With Smart Contracts by brighton36 on Wednesday March 02, 2016 @09:39PM (#11214681)

Will you be crowdfunding?

[ Parent | on HN ]

Re:Byzantine Fault Tolerant Raft With Smart Contracts by carterschonwald on Wednesday March 02, 2016 @11:27PM (#11215033)

that not currently planned, thanks for asking! But once things are a little bit more mature (with the design a bit more visibly articulated, contributions / collaborations over at https://github.com/hopper-lang/hopper will be more than welcome :)

I'm hoping to end up with a very nice tool that I hope will be used in a surprising diversity of situations, but such discussions will be more intelligible once its not just a compiler ir core and runtime :)

[ Parent | on HN ]