Pluscal tutorial

src/learning/pluscal.md

@@ -0,0 +1,4 @@
+# Learning Pluscal
+PlusCal is an algorithm language—a language for writing and debugging algorithms.  It is especially good for algorithms to be implemented with multi-threaded code.  Instead of being compiled into code, a PlusCal algorithm is translated into a TLA+ specification.  An algorithm written in PlusCal is debugged using the TLA+ tools—mainly the TLC model checker.  Correctness of the algorithm can also be proved with the TLAPS proof system, but that requires a lot of hard work and is seldom done. 
+
+The easiest way to learn pluscal, is to read the Pluscal tutorial by Lamport. Free, and readable online; it can be found here: https://lamport.azurewebsites.net/tla/tutorial/contents.html