Tezos' programming languages are growing with time. Indeed, we are seeing very interesting new ones that are created to make our developer life better and easier. This article below will consist of a short but clear summary of SOME of the current available languages that any developer can use to create Smart Contracts in Tezos.
Let's get right into and start with Michelson! (Yes, I know, some of you may prefer high level languages (I do!), but we will get to it later in this article, I promise)
Designed for smart contracts development, Michelson is a functional programming language which aims at being efficient, clear and precise for the developer. It allows for formal verification, which is basically the act of mathematically verifying a piece of code to make sure it is working as intended. Knowing this, it is easier to perform audits, for example. It is a stack-based language, meaning that a smart contract developed in Michelson will simply be a list of instructions which each have an effect on a stack, that is being passed through these instructions themselves.
Being a low-level language, Michelson can be harder to get to grips with it, however, it is a very interesting language that can be very useful if you want to know how it works behind the scenes. Developing smart contracts using Michelson helps getting a better picture of how the smart contract is actually running on the Tezos blockchain.
SmartPy was designed for lowering the barrier of entry for smart contracts development. Indeed, as you can most likely guess from the name, it is based on Python, which is a well known and "easy"-to-learn programming language thanks to its simple and clean syntax. Additionally, it also allows for functional programming, and therefore it keeps Michelson's pros such as formal verification.
Being a high-level language, SmartPy can be easier to get to grips with it. Adding the fact that Python is already famous and used by a lot of developers, it definitely helps bringing more developers to the Tezos ecosystem.
SmartPy comes with SmartPy.io, an in-browser development platform, made to ease the process of programming a smart contract in Tezos. With it, you can develop, test, analyze (and even more!) smart contracts pretty easily. Take a look at the online editor which contains some templates that you can use to play around with all the tools.
LIGO compiles to Michelson. It is a simple and clean language, which allows for formal verification as well, through a project such as Mi-Cho-Coq. With its 3 syntaxes, a developer can quickly choose the one he feels more comfortable with and start writing Tezos smart contracts.