From f2bff77ffda37e4aafc036588aef174d40b31c5e Mon Sep 17 00:00:00 2001 From: John David Pressman Date: Wed, 26 Feb 2020 03:27:11 -0800 Subject: [PATCH 1/4] Change LIGO documentation introduction to be about LIGO --- .../what-and-why.md => advanced/michelson.md} | 139 +-------------- gitlab-pages/docs/intro/ligo-intro.md | 163 ++++++++++++++++++ gitlab-pages/website/sidebars.json | 5 +- gitlab-pages/website/siteConfig.js | 2 +- 4 files changed, 176 insertions(+), 133 deletions(-) rename gitlab-pages/docs/{intro/what-and-why.md => advanced/michelson.md} (56%) create mode 100644 gitlab-pages/docs/intro/ligo-intro.md diff --git a/gitlab-pages/docs/intro/what-and-why.md b/gitlab-pages/docs/advanced/michelson.md similarity index 56% rename from gitlab-pages/docs/intro/what-and-why.md rename to gitlab-pages/docs/advanced/michelson.md index f195b97a7..9c11498b7 100644 --- a/gitlab-pages/docs/intro/what-and-why.md +++ b/gitlab-pages/docs/advanced/michelson.md @@ -1,19 +1,19 @@ --- -id: what-and-why +id: michelson-and-ligo title: Michelson and LIGO --- -Before we get into what LIGO is and why LIGO needs to exist, let us -take a look at what options the Tezos blockchain offers us out of the -box. If you want to implement smart contracts natively on Tezos, you -have to learn -[Michelson](https://tezos.gitlab.io/whitedoc/michelson.html). +Currently LIGO compiles to [Michelson](https://tezos.gitlab.io/whitedoc/michelson.html), +the native smart contract language supported by Tezos. This page explains the +relationship between LIGO and the underlying Michelson it compiles to. Understanding +Michelson is not a requirement to use LIGO, but it does become important if you want +to formally verify contracts using [Mi-Cho-Coq](https://gitlab.com/nomadic-labs/mi-cho-coq/) +or tune the performance of contracts outputted by the LIGO compiler. **The rationale and design of Michelson** -The language native to the Tezos blockchain for writing smart -contracts is *Michelson*, a Domain-Specific Language (DSL) inspired by -Lisp and Forth. This unusual lineage aims at satisfying unusual +Michelson is a Domain-Specific Language (DSL) for writing Tezos smart contracts +inspired by Lisp and Forth. This unusual lineage aims at satisfying unusual constraints, but entails some tensions in the design. First, to measure stepwise gas consumption, *Michelson is interpreted*. @@ -135,124 +135,3 @@ We cannot run Javascript on the Tezos blockchain, but we can choose LIGO, which will abstract the stack management and allow us to create readable, type-safe, and efficient smart contracts. -## LIGO for Programming Smart Contracts on Tezos - -Perhaps the most striking feature of LIGO is that it comes in -different concrete syntaxes, and even different programming -paradigms. In other words, LIGO is not defined by one syntax and one -paradigm, like imperative versus functional. - - - There is **PascaLIGO**, which is inspired by Pascal, hence is an - imperative language with lots of keywords, where values can be - locally mutated after they have been annotated with their types - (declaration). - - - There is **CameLIGO**, which is inspired by the pure subset of - [OCaml](https://ocaml.org/), hence is a functional language with - few keywords, where values cannot be mutated, but still require - type annotations (unlike OCaml, whose compiler performs almost - full type inference). - - - There is **ReasonLIGO**, which is inspired by the pure subset of - [ReasonML](https://reasonml.github.io/), which is based upon - OCaml. - -Let us decline the same LIGO contract in the three flavours above. Do -not worry if it is a little confusing at first; we will explain all -the syntax in the upcoming sections of the documentation. - - - -```pascaligo group=a -type storage is int - -type parameter is - Increment of int -| Decrement of int -| Reset - -type return is list (operation) * storage - -function main (const action : parameter; const store : storage) : return is - ((nil : list (operation)), - case action of - Increment (n) -> store + n - | Decrement (n) -> store - n - | Reset -> 0 - end) -``` - - -```cameligo group=a -type storage = int - -type parameter = - Increment of int -| Decrement of int -| Reset - -type return = operation list * storage - -let main (action, store : parameter * storage) : return = - ([] : operation list), - (match action with - Increment n -> store + n - | Decrement n -> store - n - | Reset -> 0) -``` - - -```reasonligo group=a -type storage = int; - -type parameter = - Increment (int) -| Decrement (int) -| Reset; - -type return = (list (operation), storage); - -let main = ((action, store): (parameter, storage)) : return => { - (([] : list (operation)), - (switch (action) { - | Increment (n) => store + n - | Decrement (n) => store - n - | Reset => 0})); -}; -``` - - - - - - -This LIGO contract behaves almost exactly* like the Michelson -contract we saw first, and it accepts the following LIGO expressions: -`Increment(n)`, `Decrement(n)` and `Reset`. Those serve as -`entrypoint` identification, same as `%add` `%sub` or `%default` in -the Michelson contract. - -**The Michelson contract also checks if the `AMOUNT` sent is `0`* - ---- - -## Runnable code snippets & exercises - -Some of the sections in this documentation will include runnable code snippets and exercises. Sources for those are available at -the [LIGO Gitlab repository](https://gitlab.com/ligolang/ligo). - -### Snippets -For example **code snippets** for the *Types* subsection of this doc, can be found here: -`gitlab-pages/docs/language-basics/src/types/**` - -### Exercises -Solutions to exercises can be found e.g. here: `gitlab-pages/docs/language-basics/exercises/types/**/solutions/**` - -### Running snippets / exercise solutions -In certain cases it makes sense to be able to run/evaluate the given snippet or a solution, usually there'll be an example command which you can use, such as: - -```shell -ligo evaluate-value -s pascaligo gitlab-pages/docs/language-basics/src/variables-and-constants/const.ligo age -# Outputs: 25 -``` diff --git a/gitlab-pages/docs/intro/ligo-intro.md b/gitlab-pages/docs/intro/ligo-intro.md new file mode 100644 index 000000000..c66b8b8eb --- /dev/null +++ b/gitlab-pages/docs/intro/ligo-intro.md @@ -0,0 +1,163 @@ +--- +id: introduction +title: Introduction To LIGO +--- + +LIGO is a programming language for writing [Tezos](https://tezos.com/) smart contracts. + +If we had to describe the philosophy of LIGO in a few sentences, it would be this: + +1. Design a clean, simple language with no extraneous parts or additions. + +2. Give that language multiple syntaxes borrowed from other languages so users don't +have to clutter their brain with Yet Another Notation for the same programming +concepts we've been using since the 1980's. + +3. Have that simple language encourage people to write simple code, so that it's +easy to formally verify the compiled output using a project like [Mi-Cho-Coq](https://gitlab.com/nomadic-labs/mi-cho-coq/). + +4. Stop waking up in the morning to find that your smart contract lost all its money +to some [stupid exploit](https://www.wired.com/2016/06/50-million-hack-just-showed-dao-human/). + +We can elaborate on each: + +* **Clean and simple** — Programming languages for making video games or websites +tend to prioritize accumulating a vast number of features, they're big languages for +making big projects. You use an army of mediocre programmers to write thousands +and thousands of lines of code, and then accelerate development by including dozens +or hundreds of unvetted dependencies; each of which provides an opportunity to +introduce a security exploit or insert malicious code. That's fine for a game, but +we don't think that's a very intelligent way to write a smart contract. Most useful +smart contracts can express their core functionality in under a thousand lines of +code, and the problem domain necessitates that you get as close as possible to +the minimal code size and resource use. LIGO is a functional language designed +to include the features you need, avoiding patterns that make formal verification +hard. + +* **Multiple Syntaxes** — LIGO provides three syntaxes for users which express the +same underlying language semantics. PascaLIGO is an imperative syntax based on +[Pascal](https://en.wikipedia.org/wiki/Pascal_%28programming_language%29), CameLIGO +is a syntax which closely mimics the look and feel of [OCaml](https://en.wikipedia.org/wiki/OCaml), +and ReasonLIGO is based on Facebook's JavaScript-flavored [ReasonML](https://reasonml.github.io/) syntax. + +* **Simple Code & Formal Verification** — LIGO doesn't use an object oriented paradigm, +currently code is organized using functions. While LIGO plans to have a module system +in the future, it's not the intent that this be used to create npm style cathedrals +of logical mystery meat. Once a contract is put on the blockchain, it's not possible +to change it. A new version can be uploaded, but the original contract remains +available. This makes formal verification of contract logic attractive. When the +cost of bugs is extreme and patches aren't possible it pays to get things right +the first time. + +## LIGO for Programming Smart Contracts on Tezos + +Perhaps the most striking feature of LIGO is that it comes in +different concrete syntaxes, and even different programming +paradigms. In other words, LIGO is not defined by one syntax and one +paradigm, like imperative versus functional. + + - There is **PascaLIGO**, which is inspired by Pascal, hence is an + imperative language with lots of keywords, where values can be + locally mutated after they have been annotated with their types + (declaration). + + - There is **CameLIGO**, which is inspired by the pure subset of + [OCaml](https://ocaml.org/), hence is a functional language with + few keywords, where values cannot be mutated, but still require + type annotations (unlike OCaml, whose compiler performs almost + full type inference). + + - There is **ReasonLIGO**, which is inspired by the pure subset of + [ReasonML](https://reasonml.github.io/), which is based upon + OCaml. + +Let's define some LIGO contract in the three flavours above. Do +not worry if it is a little confusing at first; we will explain all +the syntax in the upcoming sections of the documentation. + + + +```pascaligo group=a +type storage is int + +type parameter is + Increment of int +| Decrement of int +| Reset + +type return is list (operation) * storage + +function main (const action : parameter; const store : storage) : return is + ((nil : list (operation)), + case action of + Increment (n) -> store + n + | Decrement (n) -> store - n + | Reset -> 0 + end) +``` + + +```cameligo group=a +type storage = int + +type parameter = + Increment of int +| Decrement of int +| Reset + +type return = operation list * storage + +let main (action, store : parameter * storage) : return = + ([] : operation list), + (match action with + Increment n -> store + n + | Decrement n -> store - n + | Reset -> 0) +``` + + +```reasonligo group=a +type storage = int; + +type parameter = + Increment (int) +| Decrement (int) +| Reset; + +type return = (list (operation), storage); + +let main = ((action, store): (parameter, storage)) : return => { + (([] : list (operation)), + (switch (action) { + | Increment (n) => store + n + | Decrement (n) => store - n + | Reset => 0})); +}; +``` + + +This LIGO contract accepts the following LIGO expressions: +`Increment(n)`, `Decrement(n)` and `Reset`. Those serve as +`entrypoint` identification. + +--- + +## Runnable code snippets & exercises + +Some of the sections in this documentation will include runnable code snippets and exercises. Sources for those are available at +the [LIGO Gitlab repository](https://gitlab.com/ligolang/ligo). + +### Snippets +For example **code snippets** for the *Types* subsection of this doc, can be found here: +`gitlab-pages/docs/language-basics/src/types/**` + +### Exercises +Solutions to exercises can be found e.g. here: `gitlab-pages/docs/language-basics/exercises/types/**/solutions/**` + +### Running snippets / exercise solutions +In certain cases it makes sense to be able to run/evaluate the given snippet or a solution, usually there'll be an example command which you can use, such as: + +```shell +ligo evaluate-value -s pascaligo gitlab-pages/docs/language-basics/src/variables-and-constants/const.ligo age +# Outputs: 25 +``` diff --git a/gitlab-pages/website/sidebars.json b/gitlab-pages/website/sidebars.json index 1f5fec284..bde7acba5 100644 --- a/gitlab-pages/website/sidebars.json +++ b/gitlab-pages/website/sidebars.json @@ -1,6 +1,6 @@ { "docs": { - "Intro": ["intro/what-and-why", "intro/installation", "intro/editor-support"], + "Intro": ["intro/introduction", "intro/installation", "intro/editor-support"], "Language Basics": [ "language-basics/types", "language-basics/constants-and-variables", @@ -18,7 +18,8 @@ "advanced/timestamps-addresses", "advanced/entrypoints-contracts", "advanced/include", - "advanced/first-contract" + "advanced/first-contract", + "advanced/michelson-and-ligo" ], "API & Reference": [ "api/cli-commands", diff --git a/gitlab-pages/website/siteConfig.js b/gitlab-pages/website/siteConfig.js index d98334e97..9691d6697 100644 --- a/gitlab-pages/website/siteConfig.js +++ b/gitlab-pages/website/siteConfig.js @@ -23,7 +23,7 @@ const siteConfig = { headerLinks: [ { href: 'https://ide.ligolang.org/', label: 'Try Online' }, { doc: 'intro/installation', label: 'Install' }, - { doc: 'intro/what-and-why', label: 'Docs' }, + { doc: 'intro/introduction', label: 'Docs' }, { doc: 'tutorials/get-started/tezos-taco-shop-smart-contract', label: 'Tutorials' From f62ea8e8fe6e382d13726b53ba0454f8e26f8dd1 Mon Sep 17 00:00:00 2001 From: John David Pressman Date: Thu, 27 Feb 2020 19:50:25 -0800 Subject: [PATCH 2/4] Make new intro page use less 'we' --- gitlab-pages/docs/intro/ligo-intro.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/gitlab-pages/docs/intro/ligo-intro.md b/gitlab-pages/docs/intro/ligo-intro.md index c66b8b8eb..87a9bf7ba 100644 --- a/gitlab-pages/docs/intro/ligo-intro.md +++ b/gitlab-pages/docs/intro/ligo-intro.md @@ -5,7 +5,7 @@ title: Introduction To LIGO LIGO is a programming language for writing [Tezos](https://tezos.com/) smart contracts. -If we had to describe the philosophy of LIGO in a few sentences, it would be this: +The LIGO philosophy can be described in a few bullet points: 1. Design a clean, simple language with no extraneous parts or additions. @@ -19,7 +19,7 @@ easy to formally verify the compiled output using a project like [Mi-Cho-Coq](ht 4. Stop waking up in the morning to find that your smart contract lost all its money to some [stupid exploit](https://www.wired.com/2016/06/50-million-hack-just-showed-dao-human/). -We can elaborate on each: +Lets expand on each: * **Clean and simple** — Programming languages for making video games or websites tend to prioritize accumulating a vast number of features, they're big languages for From 9791b993d2a485c98709f55255277db62e41cde6 Mon Sep 17 00:00:00 2001 From: John David Pressman Date: Mon, 2 Mar 2020 21:42:45 -0800 Subject: [PATCH 3/4] Abbreviate and de-tone LIGO introduction draft --- gitlab-pages/docs/intro/ligo-intro.md | 51 ++++++++++----------------- src/test/md_file_tests.ml | 2 +- 2 files changed, 20 insertions(+), 33 deletions(-) diff --git a/gitlab-pages/docs/intro/ligo-intro.md b/gitlab-pages/docs/intro/ligo-intro.md index 87a9bf7ba..d5eb5a9ac 100644 --- a/gitlab-pages/docs/intro/ligo-intro.md +++ b/gitlab-pages/docs/intro/ligo-intro.md @@ -7,11 +7,10 @@ LIGO is a programming language for writing [Tezos](https://tezos.com/) smart con The LIGO philosophy can be described in a few bullet points: -1. Design a clean, simple language with no extraneous parts or additions. +1. Design a clean, simple language with no unnecessary parts. -2. Give that language multiple syntaxes borrowed from other languages so users don't -have to clutter their brain with Yet Another Notation for the same programming -concepts we've been using since the 1980's. +2. Give that language multiple syntaxes borrowed from other languages. Ideally +LIGO requires the user to learn almost no new syntax. 3. Have that simple language encourage people to write simple code, so that it's easy to formally verify the compiled output using a project like [Mi-Cho-Coq](https://gitlab.com/nomadic-labs/mi-cho-coq/). @@ -19,35 +18,23 @@ easy to formally verify the compiled output using a project like [Mi-Cho-Coq](ht 4. Stop waking up in the morning to find that your smart contract lost all its money to some [stupid exploit](https://www.wired.com/2016/06/50-million-hack-just-showed-dao-human/). -Lets expand on each: +The current trend in language design is more, more, more, so this might seem +counterintuitive. However most useful smart contracts can express their core +functionality in under a thousand lines of code. The problem domain +necessitates that you get as close as possible to the minimal code size and +resource use. LIGO is a functional language designed to include the features +you need, while avoiding patterns that make formal verification hard. -* **Clean and simple** — Programming languages for making video games or websites -tend to prioritize accumulating a vast number of features, they're big languages for -making big projects. You use an army of mediocre programmers to write thousands -and thousands of lines of code, and then accelerate development by including dozens -or hundreds of unvetted dependencies; each of which provides an opportunity to -introduce a security exploit or insert malicious code. That's fine for a game, but -we don't think that's a very intelligent way to write a smart contract. Most useful -smart contracts can express their core functionality in under a thousand lines of -code, and the problem domain necessitates that you get as close as possible to -the minimal code size and resource use. LIGO is a functional language designed -to include the features you need, avoiding patterns that make formal verification -hard. - -* **Multiple Syntaxes** — LIGO provides three syntaxes for users which express the -same underlying language semantics. PascaLIGO is an imperative syntax based on -[Pascal](https://en.wikipedia.org/wiki/Pascal_%28programming_language%29), CameLIGO -is a syntax which closely mimics the look and feel of [OCaml](https://en.wikipedia.org/wiki/OCaml), -and ReasonLIGO is based on Facebook's JavaScript-flavored [ReasonML](https://reasonml.github.io/) syntax. - -* **Simple Code & Formal Verification** — LIGO doesn't use an object oriented paradigm, -currently code is organized using functions. While LIGO plans to have a module system -in the future, it's not the intent that this be used to create npm style cathedrals -of logical mystery meat. Once a contract is put on the blockchain, it's not possible -to change it. A new version can be uploaded, but the original contract remains -available. This makes formal verification of contract logic attractive. When the -cost of bugs is extreme and patches aren't possible it pays to get things right -the first time. +For example LIGO doesn't use an object oriented paradigm, currently code is +organized using functions. While LIGO plans to have a module system in the +future, we don't want programs to have thousands of dependencies. Once a +contract is put on the blockchain, it's not possible to change it. A new +version can be uploaded, but the original contract remains available. Contracts +tend to control money. In that environment it's not responsible to encourage +users to incorporate lots of code from strangers. The immutability of contracts +make formal verification of contract logic attractive. The eventual goal is +to make it easy to compile a LIGO contract to a format that can be loaded into +the [Coq proof assistant](https://coq.inria.fr/). ## LIGO for Programming Smart Contracts on Tezos diff --git a/src/test/md_file_tests.ml b/src/test/md_file_tests.ml index c728a929d..ca3eb65e3 100644 --- a/src/test/md_file_tests.ml +++ b/src/test/md_file_tests.ml @@ -92,7 +92,7 @@ let md_files = [ "/gitlab-pages/docs/tutorials/get-started/tezos-taco-shop-payout.md"; "/gitlab-pages/docs/intro/installation.md"; "/gitlab-pages/docs/intro/editor-support.md"; - "/gitlab-pages/docs/intro/what-and-why.md"; + "/gitlab-pages/docs/intro/ligo-intro.md"; "/gitlab-pages/docs/language-basics/math-numbers-tez.md"; "/gitlab-pages/docs/language-basics/functions.md"; "/gitlab-pages/docs/language-basics/boolean-if-else.md"; From 15b3dc02db431f7618548862f461e12c321609ba Mon Sep 17 00:00:00 2001 From: John David Pressman Date: Thu, 5 Mar 2020 20:22:43 -0800 Subject: [PATCH 4/4] Improve LIGO intro page based on Sander's suggestions --- gitlab-pages/docs/intro/ligo-intro.md | 73 +++++++++++---------------- 1 file changed, 30 insertions(+), 43 deletions(-) diff --git a/gitlab-pages/docs/intro/ligo-intro.md b/gitlab-pages/docs/intro/ligo-intro.md index d5eb5a9ac..09da92f2a 100644 --- a/gitlab-pages/docs/intro/ligo-intro.md +++ b/gitlab-pages/docs/intro/ligo-intro.md @@ -4,59 +4,46 @@ title: Introduction To LIGO --- LIGO is a programming language for writing [Tezos](https://tezos.com/) smart contracts. +Smart contracts are a unique domain with extreme resource constraints and even +more extreme security risks. Unlike desktop, mobile, or web +application development smart contracts cannot rely on cheap CPU time and memory. +All resources used by contracts are expensive, and tracked as 'gas costs'. Smart +contracts often directly control money or assets, which if stolen could rack up to +a large financial loss to the contracts controllers and users. Tezos smart contracts +live on the blockchain forever, if there's a bug in them they can't be patched or +amended. Naturally under these conditions it's not possible to develop smart contracts +the way we're used to developing user facing applications. -The LIGO philosophy can be described in a few bullet points: +LIGO is designed with these problems in mind. The design philosophy can be +described in a few bullet points: -1. Design a clean, simple language with no unnecessary parts. +1. Make a clean, simple language with no unnecessary parts. -2. Give that language multiple syntaxes borrowed from other languages. Ideally -LIGO requires the user to learn almost no new syntax. +2. Offer multiple familiar syntaxes so users can get up and running quickly. -3. Have that simple language encourage people to write simple code, so that it's -easy to formally verify the compiled output using a project like [Mi-Cho-Coq](https://gitlab.com/nomadic-labs/mi-cho-coq/). +3. Encourage people to write simple code, so that it's easy to formally verify the +compiled output using a project like [Mi-Cho-Coq](https://gitlab.com/nomadic-labs/mi-cho-coq/). -4. Stop waking up in the morning to find that your smart contract lost all its money -to some [stupid exploit](https://www.wired.com/2016/06/50-million-hack-just-showed-dao-human/). +4. Significantly reduce the risk that your smart contract will lose its balance to an [avoidable exploit](https://www.wired.com/2016/06/50-million-hack-just-showed-dao-human/). -The current trend in language design is more, more, more, so this might seem -counterintuitive. However most useful smart contracts can express their core -functionality in under a thousand lines of code. The problem domain -necessitates that you get as close as possible to the minimal code size and -resource use. LIGO is a functional language designed to include the features -you need, while avoiding patterns that make formal verification hard. +LIGO is a functional language designed to include the features you need, while +avoiding patterns that make formal verification hard. Most useful smart contracts +can express their core functionality in under a thousand lines of code. This makes +them a good target for formal methods, and what can't be easily proven can at least +be extensively tested. The simplicity of LIGO also keeps its compiled output +unbloated. Our hope is to have a simple, strongly typed language with a low footprint. -For example LIGO doesn't use an object oriented paradigm, currently code is -organized using functions. While LIGO plans to have a module system in the -future, we don't want programs to have thousands of dependencies. Once a -contract is put on the blockchain, it's not possible to change it. A new -version can be uploaded, but the original contract remains available. Contracts -tend to control money. In that environment it's not responsible to encourage -users to incorporate lots of code from strangers. The immutability of contracts -make formal verification of contract logic attractive. The eventual goal is -to make it easy to compile a LIGO contract to a format that can be loaded into -the [Coq proof assistant](https://coq.inria.fr/). +LIGO currently offers three syntaxes: -## LIGO for Programming Smart Contracts on Tezos + - **PascaLIGO**, a syntax inspired by Pascal which provides an + imperative developer experience. -Perhaps the most striking feature of LIGO is that it comes in -different concrete syntaxes, and even different programming -paradigms. In other words, LIGO is not defined by one syntax and one -paradigm, like imperative versus functional. + - **CameLIGO**, an [OCaml]((https://ocaml.org/)) inspired + syntax that allows you to write in a functional style. - - There is **PascaLIGO**, which is inspired by Pascal, hence is an - imperative language with lots of keywords, where values can be - locally mutated after they have been annotated with their types - (declaration). - - - There is **CameLIGO**, which is inspired by the pure subset of - [OCaml](https://ocaml.org/), hence is a functional language with - few keywords, where values cannot be mutated, but still require - type annotations (unlike OCaml, whose compiler performs almost - full type inference). - - - There is **ReasonLIGO**, which is inspired by the pure subset of - [ReasonML](https://reasonml.github.io/), which is based upon - OCaml. + - **ReasonLIGO**, an [ReasonML]((https://reasonml.github.io/)) inspired syntax + that builds on the strong points of OCaml. It aims to be familiar for those + coming from JavaScript. Let's define some LIGO contract in the three flavours above. Do not worry if it is a little confusing at first; we will explain all