* [Caml-list] Blockchains in OCaml @ 2016-10-06 3:59 Arthur Breitman 2016-10-10 14:00 ` Van Chan Ngo 0 siblings, 1 reply; 6+ messages in thread From: Arthur Breitman @ 2016-10-06 3:59 UTC (permalink / raw) To: caml-list, ocaml-jobs [-- Attachment #1: Type: text/plain, Size: 1650 bytes --] Since blockchains tend to be a hot topic these days*, I am pleased to announce that OCaml is also present in this domain with the Tezos project. Tezos is a cryptographic ledger (in the same vein as Bitcoin or Ethereum) written from scratch entirely in OCaml, in partnership with OCamlPro. We are lucky to rely on some great OCaml libraries like Irmin and Lwt, and have contributed some libraries of our own like ocplib-json-typed (for reliable manipulation of JSON values) and ocplib-resto (for type safe HTTP/JSON RPCs). Tezos is a self-amending ledger. While other protocols achieve consensus about the state of their transactions, Tezos reaches a meta-consensus about its own protocol. This allows us to gradually build governance rules into the ledger by letting the participants choose under which condition the protocol may be amended. We start with a simple voting procedure to accept or reject a proposed patch to a set of OCaml modules representing the protocol. Over time, complex rules can evolve. For instance, we may introduce a form of constitutionalism by having the protocol require and enforce that any proposed modification be formally verified and guaranteed to preserve specific properties. If you find this intriguing and enjoy working in OCaml, please reach out: we're hiring! If you lean on the academic side and have experience with formal verification, reach out as well! We'd be interested in proving the correctness of some aspects of the protocol or sponsoring research in the field in general (within our modest means). Best, Arthur * perhaps hotter than it ought to be but, past the hype, there remains susbtance [-- Attachment #2: Type: text/html, Size: 6484 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Blockchains in OCaml 2016-10-06 3:59 [Caml-list] Blockchains in OCaml Arthur Breitman @ 2016-10-10 14:00 ` Van Chan Ngo 2017-12-25 13:28 ` Viet Le 0 siblings, 1 reply; 6+ messages in thread From: Van Chan Ngo @ 2016-10-10 14:00 UTC (permalink / raw) To: Arthur Breitman; +Cc: caml-list, ocaml-jobs [-- Attachment #1: Type: text/plain, Size: 726 bytes --] Hi Arthur, It is interesting to implement blockchains in functional language like OCaml. I am happy to hear more about this project. FYI, a related work, we are in progress to formalize the Ethereum Virtual Machine (EVM, the running environment of smart contracts) in Coq. Best, -Chan > On Oct 5, 2016, at 11:59 PM, Arthur Breitman <arthurb@tezos.com> wrote: > > If you find this intriguing and enjoy working in OCaml, please reach out: we're hiring! If you lean on the academic side and have experience with formal verification, reach out as well! We'd be interested in proving the correctness of some aspects of the protocol or sponsoring research in the field in general (within our modest means). > [-- Attachment #2: Type: text/html, Size: 1777 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Blockchains in OCaml 2016-10-10 14:00 ` Van Chan Ngo @ 2017-12-25 13:28 ` Viet Le 2017-12-26 14:03 ` Van Chan Ngo 2017-12-27 22:09 ` Fabrice Le Fessant 0 siblings, 2 replies; 6+ messages in thread From: Viet Le @ 2017-12-25 13:28 UTC (permalink / raw) To: Van Chan Ngo; +Cc: Arthur Breitman, OCaml Mailing List, ocaml-jobs [-- Attachment #1: Type: text/plain, Size: 1400 bytes --] Hi all, Only one year after this message, I found interest in building a blockchain and smart contracts in OCaml. May I know how far is the EVM formalisation in Coq? There aren't many materials / blockchain implementations in OCaml but I found some interesting links: https://github.com/LaurentMazare/btc-ocaml http://www.liquidity-lang.org/ https://github.com/tezos/tezos https://github.com/pirapira/eth-isabelle https://github.com/pirapira/ethereum-formal-verification-overview I would like to know more if anyone has more information. Thanks, Viet On 10 October 2016 at 15:00, Van Chan Ngo <chan.ngo2203@gmail.com> wrote: > Hi Arthur, > > It is interesting to implement blockchains in functional language like > OCaml. I am happy to hear more about this project. > > FYI, a related work, we are in progress to formalize the Ethereum Virtual > Machine (EVM, the running environment of smart contracts) in Coq. > > Best, > -Chan > > > On Oct 5, 2016, at 11:59 PM, Arthur Breitman <arthurb@tezos.com> wrote: > > If you find this intriguing and enjoy working in OCaml, please reach out: > we're hiring! If you lean on the academic side and have experience with > formal verification, reach out as well! We'd be interested in proving the > correctness of some aspects of the protocol or sponsoring research in the > field in general (within our modest means). > > > -- Kind regards, Viet [-- Attachment #2: Type: text/html, Size: 3090 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Blockchains in OCaml 2017-12-25 13:28 ` Viet Le @ 2017-12-26 14:03 ` Van Chan Ngo 2017-12-27 15:41 ` Viet Le 2017-12-27 22:09 ` Fabrice Le Fessant 1 sibling, 1 reply; 6+ messages in thread From: Van Chan Ngo @ 2017-12-26 14:03 UTC (permalink / raw) To: Viet Le; +Cc: Arthur Breitman, OCaml Mailing List, ocaml-jobs [-- Attachment #1: Type: text/plain, Size: 2484 bytes --] Hi Viet, I did not work on the formalization of EVM a while ago due to other work (automatic resource bound analysis for probabilistic programs https://channgo2203.github.io/pdfs/cmutr02.pdf) The following is the implementation (not completed) on Github. https://github.com/channgo2203/fevm However, we are working on the other aspect of EVM code analysis. We want to statically infer an upper-bound on the amount of gas consumption for all inputs (input arguments and storage configurations). This analysis is based on our previous research on resource bound analysis for both imperative and functional programs. We translate EVM byte-code into a kind of control flow graph (CFG). However, due to the unstructured and low level of EVM, I suppose it is more convenient to infer upper-bound on gas consumption at Solidity source code provided that we have a good gas consumption model for Solidity language constructs. Best, -Van Chan On Mon, Dec 25, 2017 at 8:28 AM, Viet Le <vietlq85@gmail.com> wrote: > Hi all, > > Only one year after this message, I found interest in building a > blockchain and smart contracts in OCaml. May I know how far is the EVM > formalisation in Coq? > > There aren't many materials / blockchain implementations in OCaml but I > found some interesting links: > > https://github.com/LaurentMazare/btc-ocaml > > http://www.liquidity-lang.org/ > > https://github.com/tezos/tezos > > https://github.com/pirapira/eth-isabelle > > https://github.com/pirapira/ethereum-formal-verification-overview > > I would like to know more if anyone has more information. > > Thanks, > Viet > > On 10 October 2016 at 15:00, Van Chan Ngo <chan.ngo2203@gmail.com> wrote: > >> Hi Arthur, >> >> It is interesting to implement blockchains in functional language like >> OCaml. I am happy to hear more about this project. >> >> FYI, a related work, we are in progress to formalize the Ethereum Virtual >> Machine (EVM, the running environment of smart contracts) in Coq. >> >> Best, >> -Chan >> >> >> On Oct 5, 2016, at 11:59 PM, Arthur Breitman <arthurb@tezos.com> wrote: >> >> If you find this intriguing and enjoy working in OCaml, please reach out: >> we're hiring! If you lean on the academic side and have experience with >> formal verification, reach out as well! We'd be interested in proving the >> correctness of some aspects of the protocol or sponsoring research in the >> field in general (within our modest means). >> >> >> > > > -- > Kind regards, > Viet > [-- Attachment #2: Type: text/html, Size: 5007 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Blockchains in OCaml 2017-12-26 14:03 ` Van Chan Ngo @ 2017-12-27 15:41 ` Viet Le 0 siblings, 0 replies; 6+ messages in thread From: Viet Le @ 2017-12-27 15:41 UTC (permalink / raw) To: Van Chan Ngo; +Cc: Arthur Breitman, OCaml Mailing List, ocaml-jobs [-- Attachment #1: Type: text/plain, Size: 3058 bytes --] Thanks Van Chan for sharing. I also found a solution that automatically computes the gas used by breaking down into basic computations. They are Zen Protocol: https://www.zenprotocol.com . They use F* that is very closely related to OCaml/F# to achieve their goal. So if you want to find upper-bound for EVM, I think their whitepaper is a good start. Regards, Viet On 26 December 2017 at 14:03, Van Chan Ngo <chan.ngo2203@gmail.com> wrote: > Hi Viet, > > I did not work on the formalization of EVM a while ago due to other work > (automatic resource bound analysis for probabilistic programs > https://channgo2203.github.io/pdfs/cmutr02.pdf) > The following is the implementation (not completed) on Github. > https://github.com/channgo2203/fevm > > However, we are working on the other aspect of EVM code analysis. We want > to statically infer an upper-bound on the amount of gas > consumption for all inputs (input arguments and storage configurations). > This analysis is based on our previous research on resource bound > analysis for both imperative and functional programs. > > We translate EVM byte-code into a kind of control flow graph (CFG). > However, due to the unstructured and low level of EVM, I suppose it is > more convenient to infer upper-bound on gas consumption at Solidity source > code provided that we have a good gas consumption model for > Solidity language constructs. > > Best, > -Van Chan > > > > > On Mon, Dec 25, 2017 at 8:28 AM, Viet Le <vietlq85@gmail.com> wrote: > >> Hi all, >> >> Only one year after this message, I found interest in building a >> blockchain and smart contracts in OCaml. May I know how far is the EVM >> formalisation in Coq? >> >> There aren't many materials / blockchain implementations in OCaml but I >> found some interesting links: >> >> https://github.com/LaurentMazare/btc-ocaml >> >> http://www.liquidity-lang.org/ >> >> https://github.com/tezos/tezos >> >> https://github.com/pirapira/eth-isabelle >> >> https://github.com/pirapira/ethereum-formal-verification-overview >> >> I would like to know more if anyone has more information. >> >> Thanks, >> Viet >> >> On 10 October 2016 at 15:00, Van Chan Ngo <chan.ngo2203@gmail.com> wrote: >> >>> Hi Arthur, >>> >>> It is interesting to implement blockchains in functional language like >>> OCaml. I am happy to hear more about this project. >>> >>> FYI, a related work, we are in progress to formalize the Ethereum >>> Virtual Machine (EVM, the running environment of smart contracts) in Coq. >>> >>> Best, >>> -Chan >>> >>> >>> On Oct 5, 2016, at 11:59 PM, Arthur Breitman <arthurb@tezos.com> wrote: >>> >>> If you find this intriguing and enjoy working in OCaml, please reach >>> out: we're hiring! If you lean on the academic side and have experience >>> with formal verification, reach out as well! We'd be interested in proving >>> the correctness of some aspects of the protocol or sponsoring research in >>> the field in general (within our modest means). >>> >>> >>> >> >> >> -- >> Kind regards, >> Viet >> > > -- Kind regards, Viet [-- Attachment #2: Type: text/html, Size: 6236 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Blockchains in OCaml 2017-12-25 13:28 ` Viet Le 2017-12-26 14:03 ` Van Chan Ngo @ 2017-12-27 22:09 ` Fabrice Le Fessant 1 sibling, 0 replies; 6+ messages in thread From: Fabrice Le Fessant @ 2017-12-27 22:09 UTC (permalink / raw) To: Viet Le; +Cc: Van Chan Ngo, OCaml Mailing List [-- Attachment #1: Type: text/plain, Size: 529 bytes --] On Mon, Dec 25, 2017 at 2:28 PM Viet Le <vietlq85@gmail.com> wrote: > There aren't many materials / blockchain implementations in OCaml but I > found some interesting links: > [...] > http://www.liquidity-lang.org/ > [...] > OCamlPro is doing a lot of work on blockchains these days. There is indeed Liquidity, a smart-contract language for Tezos that we already released on Github. We are also developing some tooling around Ethereum, we will probably release some parts as libraries, when they become mature enough. Fabrice [-- Attachment #2: Type: text/html, Size: 961 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2017-12-27 22:09 UTC | newest] Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2016-10-06 3:59 [Caml-list] Blockchains in OCaml Arthur Breitman 2016-10-10 14:00 ` Van Chan Ngo 2017-12-25 13:28 ` Viet Le 2017-12-26 14:03 ` Van Chan Ngo 2017-12-27 15:41 ` Viet Le 2017-12-27 22:09 ` Fabrice Le Fessant
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).