Zero-knowledge proofs (ZKPs) are a powerful cryptographic tool that can verify the correctness of computations while protecting the privacy of input data. As part of this critical infrastructure, domain-specific languages ​​(DSLs) play a vital role in simplifying the development and verification of ZKP circuits. They play an important role in bridging the gap between abstract concepts and the precise circuit representations required to prove systems.

One of the key challenges facing proof systems is translating abstract high-level concepts into real circuits. However, the advent of DSLs addresses this challenge by facilitating the structured expression of these abstract concepts in a more concrete and implementable way.

Over the past decade, we have witnessed significant growth in the number and diversity of DSLs. Activity in this area is reflected in the development of several circuit languages, including Noir, Leo, Zinc, and others. Whether you need a general-purpose option, like Circom, or a solution customized for a specific platform, like Cairo, you can choose from a wide range of languages ​​and frameworks for writing ZKP circuits.

In this article, we’ll explore the main ZK programming languages ​​that developers are actively leveraging and analyze the best features of each language.


TLDR;

Cairo By StarkWare

Cairo, the core language for general computing programs that support STARK proofs, has played a key role in the success of StarkNet and StarkEx, and has driven the scalability of applications on the Ethereum mainnet. It is worth mentioning that Cairo has played an important role in supporting various applications, including dYdX, Sorare, Immutable X, etc. The name "Cairo" comes from the abbreviation of "CPU Algebraic Intermediate Representation". In the field of zero-knowledge proofs, it plays a role similar to assembly language, making it easier for developers familiar with low-level programming languages ​​such as C, C++ or Solidity to get started.

Inspired by Rust, Cairo empowers developers to create Starknet smart contracts with a focus on security and user-friendly development. Cairo has a powerful syntax that simplifies the creation of ZK circuits, enabling users to perform a variety of tasks within Cairo programs. Additionally, a significant advantage of Cairo is its extensibility, allowing for the flexible introduction of new features and capabilities.

In ZK systems, efficiency and scalability are crucial factors, and Cairo meets this requirement by emphasizing both aspects. The language integrates optimization strategies, including constraint reduction and loop elimination, to reduce the computational burden typically associated with ZK circuits. Cairo's optimizations for circuit design lead to faster proof generation and verification, making it ideal for applications that require high throughput and minimal latency.

Cairo's expansion has been impressive, with an extraordinary surge in full-time developers over the past two years. This surge highlights Cairo’s adaptability, as Cairo’s uses are not limited to blockchain but are relevant in any context where computational verification is required. As a result, we can expect significant further growth in developer adoption of Cairo.

On September 28, 2023, Starknet launched a major upgrade of its programming language Cairo v2.3.0. This version marks a major advancement in the modularization of contracts, enhancing the potential of smart contracts by introducing new functions, storage options, and event management. The integration of these components provides a flexible way to expand contract functionality, enabling third-party modules to enhance the functionality of contracts.


Zinc by ZkSync

Zinc is a programming language designed for creating smart contracts and SNARK circuits on the zkSync platform. It adopts Rust syntax, incorporates elements of Solidity, and provides unique features.

What makes Zinc unique is its user-friendliness. You don't need to delve into all the intricacies of first-order constraint systems (R1CS) to write safe code. Zinc emphasizes immutability, making it inherently functional. This means it prioritizes immutable data and function evaluation, which reduces side effects and promotes writing cleaner, less error-prone smart contract code.

Additionally, Zinc includes safe math operations to prevent potential overflows, ensuring the safety of all operations. Although it has some limitations, such as no infinite loops and recursion, Zinc simplifies the debugging process through console log traces. These traces can simplify the transaction process of tracking and troubleshooting issues on the test network or the main network, thus improving the debugging experience.


Noir By Aztec

Noir is an open source DSL developed by Aztec, based on Rust, that aims to simplify the creation of ZK circuits and ZK programs without deep knowledge of cryptography. It is considered one of the easiest languages ​​to get started with, suitable for writing ZK applications compatible with any proof system. Noir focuses on security, simplicity, and performance. It provides a high-level Rust-like syntax that abstracts cryptographic security and simplifies the use of cryptographic primitives while maintaining high performance.

Noir has significant advantages in expanding the range of applications that can take advantage of the privacy protection capabilities provided by ZKP, thereby enhancing privacy and verification efficiency. Noir is compiled into an intermediate representation called Abstract Circuit Intermediate Representation (Acer), which can then be further compiled into R1CS. Separating the backend proof system from the language itself enables Noir to support a variety of proof systems, including Aztec Brettenberg, Turbo Plonk, and potential future integrations such as Groth16 and Halo2.

The language provides a standard library that includes efficient functions such as SHA-256 (a cryptographic hash function that produces a fixed-size output) and Pedersen-Merkle checks (a cryptographic verification technique that uses Pedersen commitments and Merkle trees to ensure data integrity and consistency). Noir is designed similarly to Rust and includes features familiar to application developers such as functions, submodules, user-defined types (structs), conditional statements, loops, and global constants. In addition, there is ongoing work on generics and first-class functions to further enhance Noir's expressiveness.

It should be noted that Noir is still a work in progress and may have some limitations and potential bugs. However, the development team is committed to continuously improving and optimizing the language.

o1js by 0(1) Labs

o1js, formerly known as SnarkyJS, is a TypeScript library developed by 0(1)Labs for creating smart contracts using the SNARK programming language. It leverages established technologies such as Node.js and browser compatibility to ensure ease of access and convenience for developers.

o1js can seamlessly integrate with JavaScript and TypeScript libraries and tools, providing developers with a strong ecosystem and broad community support. This integration simplifies the development process and reduces the learning curve of adopting a new development environment. In addition, it fully supports Visual Studio Code (VS Code), a widely used code editor, allowing developers to take full advantage of features such as code completion, syntax highlighting, and debugging to improve the development experience.

o1js is essentially a versatile ZK framework that provides you with the key tools you need to create zk proofs. It supports the creation of diverse ZK programs, covering a variety of built-in provable operations, including basic arithmetic, hashing, signatures, Boolean operations, comparisons, and more. With the o1js framework, you can build zkApps on Mina Protocol, which are smart contracts executed on the client side with private inputs.

It is worth mentioning that in early September 2023, the 0(1)Labs team announced that they would transition from SnarkyJS to o1js, and emphasized their commitment to improved performance. Of particular note, they achieved a 3-4x reduction in library loading time, which refers to the time required to import o1js, a process that may block the main thread. For web applications, loading time is important for both JavaScript execution timing and overall page rendering. In addition, the team also updated the Mina zkApp CLI, improved the user interface building experience, and announced that it will further improve the Archive Node API to enhance its reliability and clarity.


Leo by Aleo

The Aleo blockchain is unique in the smart contract space with its emphasis on privacy. At its core is the Leo programming language, a statically typed language inspired by Rust. Designed for private application development, Leo empowers creators who want to build secure and confidential decentralized ecosystems. What makes Leo truly unique is that it has played a pioneering role in introducing a comprehensive toolkit for general-purpose zero-knowledge applications. This toolkit includes a testing framework, package registry, import resolver, remote compiler, and theorem generator.

Leo was conceived by a team of developers led by Howard Wu who envisioned a way to empower developers to build decentralized applications that prioritize privacy and security. Leo's design draws on the principles of Rust while incorporating some JavaScript-like elements to promote familiarity and convenience during development. In addition, Leo aims to accelerate development and simplify the development process by providing an integrated testing platform, package registry, and import converter. This integration enables developers to focus on the core logic of their applications without being dragged down by infrastructure issues.

A compelling feature of Leo is its compiler, which converts programs into a low-level R1CS proof format. What makes the Leo compiler unique is its rigorous formal verification process. This verification is critical because vulnerabilities can arise at multiple stages, from initial programming to auditing and compilation. By performing rigorous mathematical checks to ensure that the compiler is consistent with the programmer's intent, Leo aims to reduce the risk of undetected bugs or potential vulnerabilities, especially in L2 contexts, ZK-rollups, or private programs on the Leo platform.


Circom by iden3

Circom, a DSL designed specifically for ZK circuit development, is the result of a collaboration between Jordi Baylina and the iden3 team. The Circom compiler is written in Rust, and its main task is to compile circuits written in the Circom language. It is worth mentioning that Circom has become the preferred choice for outstanding real-world ZK applications, such as Dark Forest and Tornado Cash. Its popularity is due to its excellent performance, including fast browser proof time through optimized WASM proofs, efficient server-side proofs through rapidsnark, and efficient on-chain verification.

However, it is important to recognize that Circom's capabilities are primarily focused on ZK circuit development, which may make it less suitable for handling a wider range of computational tasks. Developers looking for more functionality that can meet a wider range of development needs may find Circom's capabilities somewhat limited. In this case, developers may need to combine other programming languages ​​or frameworks to meet broader development needs.

Image via Circom

Circom's compatibility is primarily focused on widely used ZKP systems such as snarkjs and libsnark. While this compatibility ensures seamless integration with these widely used systems, it also means that Circom circuits inherit specific functionality and limitations associated with these dependencies. Developers who prefer or need alternative ZKP systems may face compatibility challenges or need to invest additional work to adapt and integrate Circom-generated circuits into their preferred systems.


Lurk by Lurk Lab

Lurk is a statically scoped Lisp dialect influenced by Scheme and Common Lisp, with a unique feature: it allows the correctness of program execution to be directly proven using zk-SNARKs, enabling compact and efficient verification.

Lurk's main uses include:

  • Verifiable computation: Lurk allows you to prove the correctness of its expressions under zero-knowledge conditions, increasing trust in the results of computations.

  • Zero-knowledge: Users can prove knowledge without revealing specific information other than the public input, thus preserving privacy.

  • Content-addressed data: Each Lurk program is equipped with a unique content identifier (CID), making it compatible with IPFS and IPLD.

  • Turing Completeness: Lurk supports the creation and proof of arbitrary computational claims.

  • Higher-order functions: Lurk functions can accept and return functions, enabling expressive functional programming.

  • Processing computations on private data: Lurk makes it possible to process private data while ensuring provably correct outputs without compromising privacy.

In building the generic circuit, Lurk took advantage of Lisp's "cons" memory allocator. This allocator merges expressions and generates references by hashing. The key is to prove that two expressions do indeed hash to the same reference. This verification enables Lurk to perform computations within the snark circuit.

Lurk is feature-rich, including support for infinite recursion, loops, conditional control flow, and multiple backend proof systems such as Groth16 with SnarkPack+ and Nova. This versatility opens the door to a variety of applications, including verifying computations, private data processing, and executing Turing-complete programs within snark circuits.


Summarize

As the diversity of ZK applications increases, there is a bright future for DSLs in the ZK space. The key to the success of DSLs is to build a thriving community and rich libraries to enrich the developer experience. DSLs that prioritize compatibility with existing libraries can leverage the knowledge and resources of the broader developer community. This approach facilitates smoother integration, accelerates development, and provides greater flexibility when implementing ZK applications. Such collaborative efforts are critical to fostering a more robust ecosystem around DSLs, providing tangible benefits to developers, and will further drive the adoption and effectiveness of ZK technology.