ZK Programming Languages: A Comprehensive Overview

Zero-Knowledge Proofs (ZKPs) are powerful cryptographic tools that verify the correctness of computations while safeguarding the privacy of their inputs. As part of this key piece of infrastructure, Domain-Specific Languages (DSLs) play a pivotal role, simplifying the development and verification of ZKP circuits. They excel in bridging the gap between abstract ideas and the precise circuit representations demanded by proof systems.

One of the key challenges faced by proof systems is the translation of abstract, high-level concepts into practical circuits. Nevertheless, DSLs step in to address this challenge by facilitating the structured expression of these abstract ideas in a more tangible and implementable form.

In the past decade, we've witnessed a substantial increase in both the quantity and diversity of DSLs. This surge in activity within this domain is evident through the development of various circuit languages, including Noir, Leo, Zinc, etc. Whether you're looking for a general-purpose option like Circom or one customized for a particular platform like Cairo, there's a wide array of languages and frameworks at your disposal for writing ZKP circuits.

In this article, we will explore the leading ZK languages that developers are actively utilizing, analyzing the best features of each language.

TLDR;

Cairo By StarkWare

Cairo, the language underpinning STARK-proven programs for general computation, plays a pivotal role in the success of StarkNet and StarkEx, facilitating the scalability of applications on the Ethereum Mainnet. Notably, it has been instrumental in supporting various applications, including dYdX, Sorare, Immutable X, and more. The name "Cairo" is a blend of "CPU Algebraic Intermediate Representation". In the realm of ZKP, it serves as the equivalent of assembly language, making it easy for C, C++, or Solidity developers familiar with low-level programming.

Drawing inspiration from Rust, Cairo empowers developers to create Starknet smart contracts with a strong focus on safety and user-friendly development. Cairo boasts a robust syntax that streamlines the creation of ZK circuits, enabling users to execute a wide range of tasks within Cairo programs. Additionally, one of Cairo's advantages lies in its extensibility, offering the flexibility to incorporate new features and functionalities.

Efficiency and scalability are paramount considerations in ZK systems, and Cairo tackles this imperative by placing a strong emphasis on both. The language integrates optimization strategies, including constraint reduction and cycle elimination, to mitigate the computational burden often linked to ZK circuits. Cairo's optimization of circuit design results in faster proof generation and verification, rendering it an ideal choice for applications demanding high throughput and minimal latency.

Cairo's expansion has been truly noteworthy, experiencing an extraordinary surge of full-time developers in the last two years. This surge underscores its adaptability, as Cairo's utility extends beyond blockchain, finding relevance in any scenario where proof of computation is essential. Consequently, the adoption of Cairo by developers is poised for even more significant growth.

On September 28, 2023, Starknet introduced noteworthy advancements in its programming language, Cairo v2.3.0. This release signifies a substantial step forward in making contracts more modular, elevating the potential of smart contracts by introducing features, storage options, and event management. The incorporation of these components offer a flexible method for expanding contract capabilities, enabling third-party modules to enhance contract functionality.

Zinc by ZkSync

Zinc is a programming language designed for crafting smart contracts and SNARK circuits on the zkSync platform. It adopts the Rust syntax, incorporates elements from Solidity, and offers unique features. Zinc ensures full type safety, allowing users to define custom types and prevent mix-ups. It also supports type inference for a more concise syntax.

What sets Zinc apart from other ZKP programming languages is its user-friendly approach. You don't need to grasp all the intricacies of the rank-one constraint system (R1CS) to write secure codes. Zinc puts a strong emphasis on immutability, making it inherently functional. This means it prioritizes immutable data and function evaluation, reducing side effects and promoting cleaner, less error-prone smart contract codes.

Furthermore, Zinc includes secure math operations to prevent potential overflows, ensuring the safety of all operations. While it has certain limitations like the absence of unbounded loops and recursion, Zinc eases debugging with console log traces. These traces simplify the process of tracking and troubleshooting transactions on testnets or mainnets, enhancing the debugging experience.

Noir By Aztec

Noir is an open source Rust-based DSL developed by Aztec to facilitate the creation of ZK circuits and ZK programs without requiring extensive knowledge of cryptography. It is considered to be the easiest language to get started with for writing ZK applications that are compatible with any proving system. Noir prioritizes safety, simplicity, and performance. It provides a high-level, rust-like syntax that abstracts cryptographic safety and simplifies the usage of cryptographic primitives while maintaining high performance.

Noir has a significant advantage in its ability to broaden the scope of applications that can utilize the privacy-preserving capabilities offered by ZKP, which enhance privacy and verification efficiency. Noir compiles into an intermediate representation known as Abstract Circuit Intermediate Representation (Acer), which can then be further compiled into R1CS. This separation of the backend proof system and the language itself enables Noir to support various proving systems, including Aztec Brettenberg, Turbo Plonk, and potential future integrations like Groth16 and Halo2.

The language provides a standard library with efficient features like SHA-256, a cryptographic hash function that generates a fixed-size output, and Pedersen-Merkle checks, which are cryptographic verification techniques for ensuring data integrity and consistency using Pedersen commitments and Merkle trees. Noir's rust-like design incorporates familiar features for app developers, including functions, submodules, user-defined types (structs), if statements, loops, and global constants. Additionally, work is ongoing to develop generics and first-class functions, further enhancing Noir's expressiveness.

It's essential to note that Noir is still a work in progress and may have limitations and potential bugs. However, the development team is committed to continuous improvement and refinement of the language.

o1js by 0(1) Labs

o1js, formerly known as SnarkyJS, is a TypeScript library created by 0(1)Labs for crafting smart contracts using the SNARK programming language. It capitalizes on established technologies such as Node.js and browser compatibility, ensuring ease of access and convenience for developers.

o1js seamlessly integrates with JavaScript and TypeScript libraries and tools, granting developers access to a robust ecosystem and extensive community support. This integration streamlines development and reduces the learning curve associated with adopting a new development environment. It also offers full support for Visual Studio Code (VS Code), a widely-used code editor, allowing developers to benefit from features such as code completion, syntax highlighting, and debugging for an enriched development experience.

Essentially, o1js serves as a versatile ZK framework that equips you with the essential tools for creating zk proofs. It enables the creation of diverse ZK programs, harnessing a wide array of built-in provable operations, including fundamental arithmetic, hashing, signatures, boolean operations, comparisons, and more. With the o1js framework, you can construct zkApps on Mina Protocol, which are smart contracts executing client-side with private inputs.

In early September 2023, the 0(1)Labs team announced the transition from SnarkyJS to o1js, emphasizing their commitment to improving performance. Notably, they achieved a 3-4X reduction in library loading time, which refers to the time it takes to import o1js, a process that can block the main thread. This loading time is particularly significant for web applications, as it affects the timing of JavaScript execution and may impact the rendering of the entire page. Additionally, the team introduced updates to the Mina zkApp CLI, enhancing the user interface building experience, and announced further enhancements to the Archive Node API, aimed at bolstering reliability and clarity.

Leo by Aleo

The Aleo blockchain stands out as a unique platform, placing a strong emphasis on privacy in the realm of smart contracts. At its core is the Leo programming language, a statically typed language inspired by Rust. Leo is purpose-built for developing private applications and serves as the backbone for creators looking to establish a secure and confidential decentralized ecosystem. What truly sets Leo apart is its 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 programming language that could empower developers to build decentralized applications prioritizing privacy and security. Leo's design draws from Rust's principles while incorporating some JavaScript-like elements to foster familiarity and ease in the development process. Furthermore, Leo seeks to expedite development by offering an integrated testing platform, package registry, and import converter, streamlining the development process. This integration allows developers to concentrate on the core logic of their applications without getting bogged down by infrastructure concerns.

A noteworthy aspect of Leo is its compiler, which transforms programs into the low-level R1CS proof format. What distinguishes Leo's compiler is its rigorous formal verification process. This verification is vital because vulnerabilities can surface at various stages, ranging from initial programming to auditing and compilation. Through rigorous mathematical checks that ensure the compiler aligns with the programmer's intentions, Leo aims to mitigate the risk of unnoticed bugs or potential exploits, particularly in private programs within L2 contexts, ZK-rollups, or on the Leo platform.

Circom by iden3

Circom, a specialized DSL meticulously designed for ZK circuit development, is the brainchild of Jordi Baylina and the iden3 team. The Circom compiler, coded in Rust, serves the purpose of compiling circuits authored in the Circom language. Notably, Circom has been the preferred choice for prominent ZK applications in real-world use cases, such as Dark Forest and Tornado Cash. Its popularity is attributed to its impressive performance metrics, featuring rapid browser proving times courtesy of optimized WASM proofs, fast server-side proving via rapidsnark, and highly efficient on-chain verification.

However, it's important to recognize that Circom’s functionality is primarily tailored for ZK circuit development, which might make it less suitable for handling a broader array of computational tasks. Developers in search of a more versatile language capable of accommodating a wider scope of development requirements may perceive Circom's capabilities as somewhat constrained. In such scenarios, developers may need to complement Circom with other programming languages or frameworks to cater to their broader development needs.

Image via Circom

Circom's compatibility centers primarily around widely-used ZKP systems like snarkjs and libsnark. While this compatibility ensures seamless integration with these widely-used systems, it also means that Circom circuits inherit specific features and limitations associated with these dependencies. Developers who prefer or require alternative ZKP systems may encounter compatibility challenges or need to invest additional effort 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 characteristic: it allows for direct proof of correct program execution using zk-SNARKs, resulting in succinct and efficient verification.

Primary use cases of Lurk:

Verifiable Computation: Lurk allows you to prove the correctness of its expressions in zero-knowledge, enhancing trust in computation results.
Zero Knowledge: Users can prove knowledge without revealing specifics beyond public inputs, preserving privacy.
Content Addressable Data: Every 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.
High-Order Functions: Lurk functions can accept and return functions, enabling expressive functional programming.
Computation Over Private Data: Lurk enables the processing of private data while ensuring provably correct outputs without compromising privacy.

In constructing a universal circuit, Lurk harnesses the power of Lisp's "cons" memory allocator. This allocator merges expressions and produces a reference via hashing. The key lies in demonstrating that two expressions indeed hash to an identical reference. This verification enables Lurk to execute computations within a snark circuit.

Lurk's capabilities are extensive, including support for unbounded recursion, loops, conditional control flow, and multiple backend proving systems such as Groth16 with SnarkPack+ and Nova. This versatility opens the door to various applications, including verified computations, private data processing, and executing Turing-complete programs within a snark circuit.

Final Thoughts

To wrap up, the landscape of DSLs for ZK is poised for expansion as ZK applications diversify. The key to success for DSL is building thriving communities and comprehensive libraries that enrich the developer experience. DSLs that prioritize compatibility with existing libraries can harness the collective knowledge and resources of the broader developer community. This approach fosters smoother integration, accelerated development, and greater adaptability when implementing ZK applications. Collaborative efforts of this nature are instrumental in nurturing a more robust ecosystem around DSLs, offering tangible benefits to developers and will further the adoption and effectiveness of ZK technology.