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 4a68141da..9c11498b7 100644
--- a/gitlab-pages/docs/intro/what-and-why.md
+++ b/gitlab-pages/docs/advanced/michelson.md
@@ -1,21 +1,19 @@
 ---
-id: what-and-why
+id: michelson-and-ligo
 title: Michelson and LIGO
 ---
 
-import Syntax from '@theme/Syntax';
-
-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*.
@@ -137,131 +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.
-
-
-<Syntax syntax="pascaligo">
-
-```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)
-```
-
-</Syntax>
-<Syntax syntax="cameligo">
-
-```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)
-```
-
-</Syntax>
-<Syntax syntax="reasonligo">
-
-```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}));
-};
-```
-
-</Syntax>
-
-
-
-<!--
-> 💡 You can find the Michelson compilation output of the contract -->
-<!--above in **`ligo-counter.tz`** -->
-
-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..b2dda419f
--- /dev/null
+++ b/gitlab-pages/docs/intro/ligo-intro.md
@@ -0,0 +1,155 @@
+---
+id: introduction
+title: Introduction To LIGO
+---
+
+import Tabs from '@theme/Tabs';
+import TabItem from '@theme/TabItem';
+
+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.
+
+LIGO is designed with these problems in mind. The design philosophy can be
+described in a few bullet points:
+
+1. Make a clean, simple language with no unnecessary parts.
+
+2. Offer multiple familiar syntaxes so users can get up and running quickly.
+
+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. 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/).
+
+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.
+
+LIGO currently offers three syntaxes:
+
+  - **PascaLIGO**, a syntax inspired by Pascal which provides an
+    imperative developer experience.
+
+  - **CameLIGO**, an [OCaml]((https://ocaml.org/)) inspired
+    syntax that allows you to write in a functional style.
+
+  - **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
+the syntax in the upcoming sections of the documentation.
+
+
+<Tabs
+  defaultValue="pascaligo"
+  values={[
+    { label: 'PascaLIGO', value: 'pascaligo', },
+    { label: 'CameLIGO', value: 'cameligo', },
+    { label: 'ReasonLIGO', value: 'reasonligo', },
+  ]
+}>
+<TabItem value="pascaligo">
+
+```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)
+```
+
+</TabItem>
+<TabItem value="cameligo">
+
+```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)
+```
+
+</TabItem>
+<TabItem value="reasonligo">
+
+```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}));
+};
+```
+
+</TabItem>
+</Tabs>
+
+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/docusaurus.config.js b/gitlab-pages/website/docusaurus.config.js
index d94dd362b..5fd7c6ddd 100644
--- a/gitlab-pages/website/docusaurus.config.js
+++ b/gitlab-pages/website/docusaurus.config.js
@@ -153,7 +153,7 @@ const siteConfig = {
       links: [
         { href: 'https://ide.ligolang.org/', label: 'Try Online' },
         { to: 'docs/intro/installation', label: 'Install' },
-        { to: 'docs/intro/what-and-why', label: 'Docs' },
+        { to: 'docs/intro/introduction', label: 'Docs' },
         {
           to: 'docs/tutorials/get-started/tezos-taco-shop-smart-contract',
           label: 'Tutorials'
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/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";