more intro material

src/learning/intro.md

@@ -1,8 +1,17 @@
 # Learning TLA+ and Model Checking
+This page lists some external resources one could use to learn more about TLA+ and related topics.
 
-* [Specyfing systems](https://lamport.azurewebsites.net/tla/book.html): by Leslie Lamport is still the reference book for TLA+ and its tools
+First things first: 
+1. Setup your IDE. Visual Studio code with [tlaplus plugin](../using/vscode.md) is recommended.
+2. If you have questions or if you feel stuck at any point, reach out to the [community](../community.md).
 
-* [The Specification Language TLA+](https://members.loria.fr/SMerz/papers/tla+logic2008.pdf): Another good manuscript by Stephan Merz explaining TLA+ specification language:  Sect. 2 introduces TLA+ by way of a first specification of the resource allocator and illustrates the use of the tlc model checker. The logic TLA is formally defined in Sect. 3, followed by an overview of TLA+ proof rules for system verification in Sect. 4. Section 5 describes the version of set theory that underlies TLA+, including some of the constructions most frequently used for specifying data. The resource allocator example is taken up again in Sect. 6, where an improved high-level specification is given and a step towards a distributed refinement is made. Finally,Sect. 7 contains some concluding remarks
+If you want a good kickstart to TLA+, start with [Leslie Lamport — The Paxos algorithm or how to win a Turing Award. Part 1](https://www.youtube.com/watch?app=desktop&v=tw3gsBms-f8) and [Part 2](https://www.youtube.com/watch?v=8-Bc5Lqgx_c). It is a good introduction on TLA+ and uses Paxos and Consensus as an example. 
+
+Another longer, popular and more complete option is Lamport's video course available on the [website](https://lamport.azurewebsites.net/video/videos.html).
+
+[Specyfing systems](https://lamport.azurewebsites.net/tla/book.html): by Leslie Lamport is still the reference book for TLA+ and its tools. It's well written and easy to follow.
+
+* [The Specification Language TLA+](https://members.loria.fr/SMerz/papers/tla+logic2008.pdf): Another good manuscript by Stephan Merz explaining TLA+ specification language:  Sect. 2 introduces TLA+ by way of a first specification of the resource allocator and illustrates the use of the tlc model checker. The logic TLA is formally defined in Sect. 3, followed by an overview of TLA+ proof rules for system verification in Sect. 4. Section 5 describes the version of set theory that underlies TLA+, including some of the constructions most frequently used for specifying data. The resource allocator example is taken up again in Sect. 6, where an improved high-level specification is given and a step towards a distributed refinement is made. The fnal Sect. 7 contains some concluding remarks.
 
 
 ## Resources