TL;DR
Leo is a statically-typed programming language for private smart contracts designed for intuitive Aleo blockchain development. It is powered by ZK, with unique syntax to compose on-chain and off-chain logic.
What the heck is even a Leo?
Most features you’re used to from smart contracts can be expressed in Leo. You can define a cryptocurrency program which mints, transfers and airdrops tokens; you can define a voting program, or a DAO; and much more. However, in contrast to, for example, Bitcoin or Ethereum transactions, users do not send signed instructions into the network for execution. Users execute the code off-chain and send, on-chain, a zero-knowledge proof (or more technically, a SNARK) of the off-chain execution. This is possible because, under the hood, Leo program functions compile to a set of constraints (expressed in R1CS). As a result, even transactions expressing truly enormous state updates are small, can be verified ultra-fast, and, most importantly, keep user data private from the network.
Very cool bro, but why create a whole new language?
The first version of Leo was released back in 2020, making it one of the first ZK programming languages, and it still shines today on three fronts: proving speed, safety, and developer experience.
Leo Advantage #1: Fast proving speed
Despite the magic of zero-knowledge proofs, they have a drawback: they require a lot of computational power to create. A very optimistic estimate of future ZK systems is that they’ll still incur a 1000x proving overhead over native computation (assuming similar hardware). A custom “zk-friendly” “zk-DSL” language is essential to minimize the footprint of the function when expressed as constraints and to speed up proving. Despite the breathtaking and amazing progress in the last couple of years proving Solidity or Rust logic (almost) out of the box, such “zk-VM”-based approaches still lag behind on performance.
Over the last few years, many exciting new proof systems have emerged, and due to the Leo compiler’s modular nature, the existing Varuna proof system can easily be swapped with a more novel proof system, while retaining the benefit of constraint-optimized compilation.
Leo Advantage #2: Safety
The number one challenge facing blockchain developers is a lack of safety. Smart contract and bridge hacks are responsible for more losses than anything else. Expressing transactions as zero-knowledge proofs adds an extra security risk: if an invalid state becomes accepted, there could be hidden inflation, similar to the Zcash inflation bug in their proof system. In order to minimise security risks, various parts of the Aleo toolchain have been formally modeled and verified. In the future, Leo will also fulfill its promise of utilizing a formally verifying compiler. Keeping the language footprint small is essential to achieve that goal.
Cryptography researcher Thaler mentions that a big advantage of proving statements about programs built in pre-existing languages like Rust is that its creators don't have to build their own compiler. However, it’s worth taking into consideration that the majority of compiler logic of pre-existing languages is not relevant in the context of generating proofs. Rust's most complex and useful feature - memory safety - is not by itself meaningful in the context of generating a proof. Neither is language syntax related to concurrency. Going one level lower, a significant portion of compiler middleware is dedicated to hardware-independent and hardware-dependent optimizations. While these optimizations are essential if you want to prove statements about, e.g., the Rust programming language, it would be silly for a zk-VM to reflect all of that logic if you have no intention of proving statements about Rust programs. Moreover, the added logic introduces a ton of chance for bugs:
“Even with conservative estimates, every month, there should be at least a dozen new known vulnerabilities likely to lead to an exploit in a formally verified RISC-V ZKVM, where proofs are verified against assembly generated by one of the two major compilers (GCC or LLVM). This does not count unreported bugs.” (source)
Leo Advantage #3: Developer experience
Third, the developer experience. Leo's main purpose is to generate proofs on the Aleo cryptocurrency network, and its async-await syntax explicitly models moving data between an on-chain and off-chain environment.
“The unique part of Leo is that it separates transition and function. The transition is executed off-chain with privacy. The correctness of the execution is proved by a zero-knowledge proof and verified by the network. All the inputs [...] and the intermediate variables are hidden by default. The function is executed publicly on-chain so that it can read and write the public state on-chain.” - (source)
Async functions are executed publicly. Async transitions can call async functions. A call to an async function returns a Future object. It is asynchronous because the code gets executed at a later point in time. Async functions are atomic; they either succeed or fail, and the state is reverted if they fail.
Which apps can be built with Leo?
Smart contracts are powerful tools, allowing users to manipulate on-chain state without permission and powering crazy economic concepts such as Flash Loans, Time-locked Liquidity and Continuous Auctions. As Tarun mentioned, DeFi intrinsically embeds collateral reqs. By adding the power of zero-knowledge proofs, that collateral can now also be privately owned. Add oracles on top, and we can do private credit scoring, private auctions, private DeFi vaults, and much more.
Today, Aleo is live with the liquid staking protocol Pondo, Automated Market Makers, and many more applications built with Leo.
In the Future, Leo will become ever more performant, safe and easy to use.
To meet the vibrant developer community, come and follow:
Leo’s documentation: https://docs.leo-lang.org