Programming Languages in ZKP

We hosted an online session of Programming Languages in ZKP on Friday June 17, 2022. We welcomed 8 speakers and panelists from the top projects in the industry to share their perspectives.

Zero knowledge proof (ZKP) is one of the most important technologies in the blockchain space and beyond. In the last 5 to 10 years, we have seen tremendous strides on both theory and practical sides of ZKPs, but using them in applications has not been very easy for developers. Several blockchain startups and companies are working hard to address this problem.

We put together the discussion questions during the panel to present you with a holistic view of the popular topics in the space right now.

How should we choose among the variety of languages?

Shahar: 3 aspects should be considered: onboarding cost of the new language, scalability needs, and ecosystem support.

Howard: Use case is the key: decide the language based on functionalities and properties of the application. For example: choose on-chain vs off-chain wisely. Widely persistent data storing or shareable program should be on-chain, and quickly ready or one-player deterministic games should be off-chain.

Gautam: We are picking an ecosystem rather than a language. For example, with Cairo, we are actually choosing StarkWare, and with Leo we are choosing Aleo.

By design, some languages understate the fact that the underlying mechanism is a zkSNARK, for example, if it encodes a full virtual machine inside a zkSNARK circuit. The language compiles to an instruction set for the virtual machine, so developers may not be aware of the zkSNARK circuits behind. In contrast, some languages / APIs enable developers to build specialized zkSNARK circuits.

Daniel: Developers have limited choice as they are in essence choosing ecosystems with considerations like gas cost and platform specifications. In the future, developers should not be constrained by the popular domain specific languages.

Will generalized systems like zkEVM replace ZK-specific languages in the future?

Wei: zk-VM aims for scaling proposes, but domain specific languages can fit specific problems like payments better. The generalizes systems and ZK-specific languages should co-exist in the future

Shahar: CPUs can’t replace integrated circuits, just like general programs will not replace the specific languages that need to be low level and more efficient.

Gautam: VM has a large overhead with memory and traces, so not all protocols should go through a generalized system for better efficiency.

Daniel: Prover efficiency of zkEVM should not be an issue in the future with better parallelization. Sequencing is the main bottleneck currently, and languages should be chosen based on sequencing performance.

What are the challenges to verify programs written in ZKP?

Yanju: There are different ways of verification we can do. For example, indirect theorem prover and automatic formal verification.

An indirect theorem prover requires experts to specify the required properties. Automatic formal verification uses symbolic execution which converts a program from the target language to logical formulas. Developer-friendly way of writing specifications is a challenge. We do not have a big prime theory to compute the verifications efficiently.

Shahar: It is actually easier to verify programs in ZKP because after we compile the program, it cannot be changed, so we can rely on the proof to guarantee the correctness of the program.

Howard: There are two ways to think about verification for programs in this domain. First, a verifying compiler. Second, a one-shot proof for programs.

First, you want to make sure the compiler itself is outputting the correct programs by compiling and synthesizing the circuits correctly, but it has been challenging to build one.

The other domain, one-shot proof for programs, is a more tractable problem. Developers only need to make sure the program itself is synthesizing correctly based on the high-level description. However, one-shot proof might add complexity.

What is the future to develop on multiple chains with multiple languages?

Daniel: Today, the EVM is the closest thing we have to a common standard, but it is not yet the ideal language, especially for ZK-rollup

Howard: We might not end up with one great answer, but we would have many good solutions and platforms. Something similar to REST API will emerge, allowing different chains and languages to interact with each other.

How to avoid “silos” when there are multiple frameworks of languages to perform ZKP?

Joshua: Using intermediate representations, like Vamp-IR, is definitely helpful. Developers should share their artisanal tricks for writing different circuits and use them in intermediate layers.

When new proof systems come out frequently, how to balance quick adoption and security stability?

Howard: VC should fund a startup that is doing SparkNotes on ZKP systems because it is difficult to keep track of all the new proof systems. It will be beneficial to directly read about the goals, properties, and tradeoffs of a specific proof system. When PLONK first came out, there was no formal peer-review process, and it was invented out of necessity. Value of new systems might not be based on academic rigor, but is the results of the cumulated knowledge by the people in the industry.

Shahar: If the new system can provide crucial functionalities, it is worth it. Otherwise, it is better to use something foolproof.

The original recording of the talk is in our YouTube Channel: https://www.youtube.com/channel/UCM7Dc3y3BVTTpprDidVV7iw

Delendum Ventures specialize in the zero-knowledge domain and support early-stage zero-knowledge based projects with incubation and funding. The partners include renowned researchers in academia and industry professionals specializing in the zero-knowledge domain.

We host monthly panel discussions and publish research blogs. If you want to share your ideas, or seek advice, review, or co-publish, contact hello@delendum.xyz.