ZKPodcast: ZK languages with Alex Ozdemir

Transcript

[Music] welcome to xero knowledge i'm your host anna rose in this podcast we will be exploring the latest in zero knowledge research and the decentralized web as well as new paradigms that promise to change the way we interact and transact online this week i speak with alex osdemere a phd student at stanford researching formal methods cryptography and distributed systems in this conversation he shares an overview of zk languages what they do and where they live in the stack it's a bit of a bird's eye view

that might be helpful to devs who want to jump in we also talk about his recent work called cersei dealing with practical implementations of generalized computation within zk systems but before i start in i want to remind everyone that there is currently a git coin grant clr matching round on and if you want to support the zero knowledge podcast this would be a great time be sure to pop over and donate all donations are matched and so your donation can go a lot further if you donate now i've added the link to our grant in the show notes now i also want to thank this week's sponsor mina protocol mina is the world's lightest blockchain creating a private gateway between the real world and crypto the layer 1 protocol replaces the

traditional blockchain with a zero knowledge proof ensuring a super light and constant sized chain which allows participants to quickly sync and verify the network the entire chain is and always will be about 22 kilobytes even as it scales and snark-powered apps called snaps allow access to verified real-world data from any website for on-chain use the ecosystem is growing fast ahead of mina's upcoming mainnet launch with validators and community members in more than 120 countries but it's still early and there's still opportunities to get involved at the ground level to do so visit minaprotocol.com and find out more you should also check out mina's first virtual illuminate summit which is happening

on march 28th visit illuminate.minaprotocol.com to secure your spot i've also added the link to this in the show notes so thank you once again mina protocol for supporting this podcast now here is my conversation with alex osdemere all about zk languages [Music] so today i'm sitting with alex osdemir a phd student at stanford researching formal methods cryptography and distributed systems his recent work deals with practical implementations of generalized computation within zero knowledge systems but that's actually something we're going to come back to later the majority of this episode is going to be about mapping the different zk languages out

there so i want to say a big welcome to alex welcome to the show thank you anna i'm happy to be here and as you said i've been spending a lot of time lately thinking about these systems that we build to help map our ideas into zero knowledge proofs and and kind of the process of thinking about that i've been exploring all these different languages that people have cooked up and i'm excited to talk about them very cool and i think i mean i think you're a great person to have on to talk about this because of that experience i think for the majority of episodes that we've done on languages we focused in on one particular project's kind of interpretation of that um and so i think throughout this episode we will be mentioning languages

from projects that we have had on in the past or languages that we've just mentioned but i mean the reason i want to do this also on a personal level is i don't always understand where they fit like i don't understand which languages are actually competing with other languages where they're compatible if they're focused on different parts of sort of the zk stack and so this is what i'm hoping we can better understand through this interview or even i i don't know if i should call it an interview it might be a little bit more of a collaborative description something like that yeah yeah yeah i know i i think that an interesting tier to like want to look at all of them at once is totally right you

know many colleges offer these programming languages classes when you're studying computer science and i think the whole the point of that kind of class is to look at all these languages at once with the sense that like you can only really understand them in comparison to one another um and i think that's true for languages broadly construed as well i mean i guess it's even true if you study like french and english or something oftentimes you learn through contrast and the same thing is true for these snark languages cool before we kick off this kind of dive into the zk language map i i kind of want to hear a bit more about you and your background what you were doing maybe before getting into this what led you to this i think that actually sort of the the beginning of maybe me being here today was was in

college when i wasn't even aware that cryptography existed um and the thing that really fascinated me was the systems the compilers the runtime systems that people use to bring programming languages to life and i was i was hunting for an opportunity to get to learn more about that um and i kept on striking out nobody around me was working on that um and so i got kind of diverted onto a theoretical path that ultimately led me to cryptography and and then sort of serendipitously it seems like cryptography is at a point where really there are some substantial language challenges in cryptography um so i i guess in some sense i ended up where i was going all along yeah what led you to the zk space specifically though because like the cryptography

space is wider and i'm sure cryptography engineering is wider so why is your knowledge i think the answer here is kind of on the theory side um so i showed up at stanford as a sort of like a theory student and i was hanging out with other theory students and there's this really fascinating theoretical result called the pcp theorem and it's a theorem about proofs so it's something that people from zero knowledge can appreciate um you know zero knowledge says that you can write these proofs that don't reveal secrets and what the pcp theorem says is that you can write down proofs um where the verifier only has to check three bits of the whole proof so anyways it was this really interesting theoretical result and uh when i first heard it i thought

it was false it sounded like no it's absurd right like checking three bits of the whole proof there's no way that's that you're actually going to be it's going to be a valid proof then i started bumping into some of dan's students and they were telling me that actually you know not only is this true but there are actually practical systems that are built around this kind of theorem and those those systems are of course all the systems that underlie zero knowledge and so i kind of came from the hard theory angle i guess like just like being really excited that there is an application of this seemingly impossible and seemingly wild theoretical result so you're also a member of dan bonay's applied cryptography group we've actually had a few other members of that group on the show already um when did you join that group i guess

we're coming up on like a year and a half now um i started working with dan this summer after i began my phd um and i was i don't think you've had riyada here no i don't think so i was working very closely with riyad yeah and still do cool and maybe another guest for future episodes if if he's interested yeah i would encourage it yeah um okay so then let's start to scratch the surface on this topic that we want to cover maybe as a starting point though it might be good to actually explain what these languages are even for like going from maybe the developer even of an application like what what are these different languages actually supposed to do the zk languages

yeah that's a good question i i actually like to think of the question like even a little bit more broadly than that which is that let's not start at the developer let's start at the person who has the cool idea you know even if they don't know how to program right of like hey this is something that you know it's like a statement it's like something that you could imagine proving and there's some notion of secrecy and and i think that kind of the core problem for zero knowledge is that it's super powerful it gives you these great properties but it gives you these great properties in a very arithmetic world a very mathematical world you know it doesn't tell you about how to show that you know your password it tells you about how you can show that you know the solutions to some polynomial equation

there's a disconnect there like if i told my mom that she would be like what are you talking about right and so and so i guess the idea is that you know we need some compromise between what the cryptography gives us here which is this statements about equations and and between what humans can understand and i think that this is where languages come in so the idea is like okay we're going to come up with a language and it's going to be better than equations right but it's still going to be formal um and the idea is that you're going to you're going to take your thoughts and you're going to formalize them into the language and that's the work that you're going to do this is something that a developer is going to do that's going to be writing some code and then the language is compiler or the

language is implementation whatever it is it's gonna get you from that language down to a zero knowledge proof and perhaps it's gonna do that by turning the language into a bunch of equations over a finite field or something else so it's a big pipeline and we're kind of at the top side of it right we're asking how do you take the human ideas and encode them in a formal way so that can still be translated to field equations i'm actually curious as you say this what's underneath that part is that where you get into like the circuit programming languages or would you also include circuit programming languages into what you just described is it more like you're dealing with the actual computer itself and like the hardware like what's i'm kind of curious where you stop as you go down that

path where do we say yeah it's not a language anymore this is now a different problem yeah um i i guess like as somebody who likes languages i'm sort of a language maximalist so i i try to find languages anywhere anywhere you can imagine them i would say these like circuit programming systems i would call those languages too but but certainly i think by the time that you have a bunch of field equations and you're trying to prove that you know a solution to them this is no longer a language problem this is where the cryptography comes to bear and actually i work on that sometimes too and i enjoy working on that but i think that's where i would draw the cutoff point and there are lots there's lots of great

work that goes under the hood uh it goes on under the hood there that we're not going to talk about today and and this is um like i don't know if you've ever gotten ali kiesa on the podcast but he's probably the world expert in this we did but we actually had him on for starkwear not for languages so i don't know if we talked about starks yeah i know that's a great example so starks are one of the systems for saying okay i've got something like a set of equations over a finite field i want to prove that i have a solution to them starks they're one of these these lower um components that are going to allow you to do that yeah in the same way that that grot 16 or sonic or planck all of these systems that we talk about those are at the bottom of the stack

they're they're proving that you know the solution to some set of equations got it now given the kind of dynamic of this we're going to be talking more at this top level from the user developer to the actual i guess can we call that like circuit language or like what like how would you group that groth starks like what is that called we we call it yeah we call them all circuits um circuits okay yeah but when we say that we're not imagining like the kinds of digital circuits that are in your computer that evolve over time they're circuits in the sense that they take a bunch of values and and combine them and collapse them down into a single answer yes or no got it so

we're working between the user and the sort of circuit level uh but what was there in the past like what were people using to do that originally like i don't think that there were you know bespoke languages right off the bat so what would somebody have used kind of early on i guess this is this is our beginning of the language story sort of like what came first and in the very beginning people in some sense didn't care right they were just trying to show that they knew the solutions to these field equations but then once they started using it so for example the first the big original push for zcash they needed tools that were going to help them construct equations that checked in this case the zcash properties so the fact that you know the identity of some

secret coin and probably the first notable cut at this is something like gadget lib which is is sort of folded up inside the lib snark code base so so one of the earlier not the first but one of the earlier implementations and and really that was just sort of like a c plus library that allowed you to construct field equations that was that's what it was and so i don't know if you want to call that a language or not um i think maybe it's fair to say at the beginning it wasn't you know you're just you're just putting together these equations but but it's inside c plus plus and so you can start to write c plus structures on top of it like imagine you write like oh i'm going to define a c plus class that represents a boolean represented in the field so it's like

a c plus class that captures a single field element that's zero or one and i'm going to define not over it i'm going to define and over it all the boolean operations and now you start to get something that looks a little bit more like a language so that's what gadget lib it was building these gadgets that's what it was it was building these gadgets that would allow you to capture kind of c plus plus e concepts inside the circuit you just mentioned libsnark i think we did talk about that possibly when we had like howard wu on a long time ago he did sort of an intro to zk snarks and i think we potentially would have mentioned it back then but was libsnark like lib i guess stands for library yeah is that a language is that a collection of libraries is

that like i yeah i was never entirely clear on like how that was used generally when i talk about libsnark i'm talking about about the implementation of a proof system so it a code that implements that thing that goes from from a circuit to a proof but i think also gadget lib this sort of library for constructing circuits um i think that was also in the libstark code base certainly those two things were developed by the same people at the same time okay for solving kind of in the same direction i guess exactly yeah or i think of it as being useful to say that libsnark is the proof system implementation and gadget lib is the library for creating circuits okay so i think that really nicely sets

the scene for you know what we're going to talk about going forward which is a lot of the new languages and the kind of new implementations that we've seen emerge i kind of want to like hand this to you a little bit do you want to take the lead and start to share with us some of the findings of your research maybe like help us navigate and map what's out there yeah totally and and i think this is actually kind of an exciting story to tell because it really is a story so you know we started with this thing like gadget lib which was just a two plus plus library for building circuits and and people looked at it and they thought i can do better and they thought that you know ten times and we have ten ten languages that came out of it um

probably more than ten to be honest but we'll talk about what we can so i think actually the first thing that people thought when they looked at gadget lib is they thought this is great but i don't like c plus plus which i can relate to like i i write a lot of people's plus in my job and that is maybe not my favorite thing in the world to do um why is that what's what's wrong with it what's annoying about c plus plus in this context i think that most of the challenges with using c plus plus are general challenges and and they're sort of amplified by our context so let me be a little bit more specific there i think c plus it was designed now 30 40 years ago and the idea was that it didn't want to get between you and the machine

it would wanted to let you tell the machine to do anything that the machine could do and in order to enable that it doesn't have very nice abstractions it's very easy to make a lot of mistakes in that language in the years since people have come up with ways to still write very efficient programming languages that have better abstractions and so in some sense like i don't want to pick on the language it was great um and it's incredible that it's it's survived so long and it's still so widely used but but nowadays people just have other things that they like more and frankly are better they're they're just newer and you know are still seeing um their adoption get more widespread um so so normally the this actually is a good segue so normally the

the language that people use as an alternative to c plus plus is rust um which is widely used in the blockchain community and and it has that same goal it doesn't want to get between you and the machine but it just has a lot nicer actions and this is important because in blockchain security accuracy these are things that are so important so having a language that's going to have clean abstractions and help you avoid mistakes is usually useful in trying to make reliable software so one of one of the first replacements to gadget lib was was bellman which was essentially the same idea we want to make a good library for helping you construct circuits but we're going to do it in rust and and we're going to be more confident that the the library is not going to mess up um because we're using a language that

has better abstractions and so this is like zcash sapling to my knowledge bellman was developed in the course of building zcash zappling um and it has since been used more broadly but um that was that was one of the priorities of the team um when they were when they were building on sapling do you actually know who wrote bellman is it the zcash com is it them is it that team or is it a more collaborative effort it's to my knowledge it started out with them um and it has sort of become more of a community project as time has gone on um so they still contribute to it and uh the folks over at matter labs contribute to it quite a bit as well there could be others uh if i'm if i'm missing your contributions it's

ignorance not malice my apologies cool so yeah so there were these people who thought okay uh gadget live would be better if it was in rust um and also i want to say at the same time they did some other stuff on the proof system side not on the language side um so so they also re-implemented some proof systems very interesting work very very great um just not what we're talking about right now um but but you know not everyone loves rust so so people you know this is a simple idea i don't like c plus plus i want gadget live in my favorite language you can repeat that for all kinds of languages and so another project that i would place in this vein is snarky so snarky had the same idea of okay basically we're writing a library to

construct circuits now we want to do it in ocam which is a language that's very common in the programming language community and is often taught in schools some similar project i think they had slightly more ambitious goals in terms of how o'camely they wanted it to be they wanted to try to get a little bit further from the circuit in the circuit world but but on the whole kind of the same idea so yeah i i think there are a few other projects in this vein but maybe we'll we'll call it um for now and maybe say that that's kind of the end of the era of i just want a library to help me build circuits and then people started to ask hey what about languages for building circuits like is there is there some kind of good language

abstraction here and one of the the first things that comes to mind when you think about languages for circuits if you have a sort of electrical engineering background is you think about the languages that people use to build the circuits in your computer what are those actually yeah like are you talking about like the soar and sand gates and like i mean i'm i don't know i did that that very basic intro to computer science where you like build a computer from scratch but i'm curious at what level is that exactly that level right like at the you know at the lowest level the stuff in your machine is a bunch of nand gates typically some kind of some kind of binary gate and some some chunks of memory they call them

registers and and clocks but yeah i know so at the bottom level your computer is like a clock something that just goes up and down and registers things that save values until the next clock cycle and these gates and somehow that's got to be organized into a central processing unit into memory into like the floating point unit into everything right um and there are languages to help people do this so typically the the sort of industry standard here is a language called verilog or system verilog and these languages they're kind of like the wild west people don't even really call them programming languages sometimes they're called hardware description languages and the reason that they're called that is they're not really they're not for

programming they're for building these circuits and hardware um and they have sort of a different mental model for how they work but but in some sense it's kind of similar to what we're doing here right so so they're building circuits they're building these circuits that change over time but some parts of them don't change over time some of them just do math and in some sense that's what we're trying to do we're trying to build circuits that just do math we're not doing it on on booleans we're doing it on fields but like uh whatever similar enough and so um this is something that a guy named jordy balina was thinking about and so he asked hey could could we build a sort of a verilog-like language but for circuits over fields not for circuits over bits and the answers of course you can that

makes total sense right like you have gates that add and multiply and so and so the language that came out of that that line of thinking is called surcom which i think is supposed to stand for circuit compiler and it's like it's totally like verilog or system verilog except for your handling field elements we've actually had jordy on the show and i think we did talk quite a lot about circum so i'll add the link to that in the show notes if people want to hear a bit more about it yeah he's he's uh he's a great guy to talk about it with i guess he understands his language better than anybody else by a good margin yeah so where are we okay well yeah we're thinking about circle so sircom is kind of this hardware description language take on what it means to build circuits

for a proof um and and this was this was different because previous things had just been sort of libraries for building the circuits so it's like okay you went from a library for circuits to a language for circuits and and in some sense it seems like maybe this is the end of the story like great we have a language but it's not and and the reason it's not is because for those of the listeners who might have a background in electrical engineering you know i said earlier that hardware description languages and programming languages aren't really the same like they kind of work in different ways um i think anybody who's worked with both can tell you which one they like more they like programming languages so in programming languages you know we have these notions of variables that get modified we're very used to using them as

developers it's a pretty clean mental model um and verilog is crazy um like it's really hard to reason about and so it's it's not really enough to have a hardware description language for circuits really we want to be able to compile a true pro like more more advanced programming languages to circuits and so so even after surcom people were still thinking can we do better in this case though would they then build on top of circum or would they rethink that role that's a great question yeah like is it is the idea here that you're going to take c and compile it to surcom and take circum and compile it to a circuit um it's something that you could do i think i think most people said hey if

we're going to build do all this work of building a compiler to circuits that's that's a pretty challenging task we're totally happy to use a library for building the circuit like we like circom isn't going to help us that much if we're already doing this much work so they i think it's more common for these systems to build on on billman or on gadget lib or on systems that that are like very like those okay hardware description languages are not the end of of the road for languages for snarks what we really want is we want to be able to take a language like python or like rust some language that we know and love and we understand the semantics of and compile that to a circuit and and maybe we can compile

like c or rust to a circuit that would be awesome or maybe we can compile something like c or rust to a circuit that would also be good at this point there's a whole host of projects and and i'm going to talk about them in a particular order but that's not quite necessarily the order that things happened and a lot of this work was really concurrent and some of it actually was even concurrent with what we've been talking about already so so probably the first language we'll talk about here is socrates so zocrates has this cute name inspired by the greek philosopher also inspired by zero knowledge and the idea for socrates was to to be a compiler from a rust like language to a circuit and when you start thinking about building a compiler

like this there's a few things that immediately become challenging one thing that's challenging is that in a language like rust you have the idea of a variable that you can put a value in it's like a box like a variable you can think of it as a box holding values you can put a value in and then later you can take that value output another value and and so on um and and in circuits you don't really have this so that's that's a challenge that zachary's had to bridge like what does it mean when i say x equals five and later on i say actually i want x to be y like how does that get turned into a circuit um and but the people who are building socrates figured out how to handle that so that kind of gave them the notion of a variable they also wanted to capture

capture the notion of computing over things that were not finite fields so computing over booleans computing over fixed width integers these were things that previously had been tackled in the context of gadgets like i have a boolean gadget and largely zocrates used the same techniques but now to capture a language in which there was a primitive boolean type so you you interacted with the boolean just like it was a boolean you didn't interact with it um as if it was some kind of specialized gadget for booleans so i think that there's really like a big sort of usability improvement here i i go from like having to like use this arcane rust or c plus plus library that gives me a gadget from bullions

to oh i can write bool a equals whatever and and i think that even though like zachary's wasn't doing like a lot of like technical innovation in terms of the algorithms of how they turn things into circuits like the usability when here is huge and so i think they deserve a lot of credit for that and similarly other people who are working on these high-level languages where we're trying to pursue that that usability gain are there any other differences from the socrates model and what you described as like this verilog like construction that's a good question in the zocrates case specifically there is an important technical difference between the verilog-like model and socrates um which is that the verilog

model you know you're building the circuit in some sense if the machine is a circuit you are on the machine the language is not getting in your way any circuit that exists you can describe but what they did did when they started with socrates is they decided that they were going to start to restrict you and they were going to do that in in the service of coming up with a sort of a mental model of the language that was easier to understand um when you're when you're making things easier to understand often you sort of lie you cut things out uh this is good i guess you make things a little bit less flexible yeah exactly exactly you're making it you have to fall into this kind of pattern of thinking it it's almost like is it less customizable i don't know if that's the right term

but i think exactly that yeah it's less customizable like there might be some idea that you have that it's kind of a weird idea but it performs very well in a circuit exactly that's why you care about it but socrates isn't going to let you say it okay and so the critical thing here is this idea of introducing approver provided values so the whole point of zero knowledge proofs is that the prover has some secret and it's mine and it's trying to prove to you that it knows that secret and in some sense how the prover came up with the secret is not in the circuit and so in circom in the middle of your circuit you can introduce some new prover provided value that comes from nowhere and then you maybe check that it's legitimate but in zocrates that doesn't happen the prover provides

inputs and everything inside the circuit is computed from those inputs it's a little technical but i think it's actually important because it means that something like zcash you wouldn't be able to implement it nearly as efficiently in socrates because the zcash developers really spent a lot of time figuring out how to use all those provided values very strategically does it make it so that certain kinds of optimizations are harder to do or is it itself optimized enough that you don't need that i think in some sense like both of those things are true it does bar certain kinds of optimizations like many of the stuff that the zcash developer has hooked up the question like whenever you're optimizing like what's going on is you are writing code in a language

and then below that language there's a compiler that's turning it into some kind of like assembly in our case it's turning into a circuit and the compiler is trying to optimize like you know whatever whatever code you give it it wants to make the best circuit possible but then also sometimes you're thinking like hey i'm smarter than the compiler i know something special about my problem and you're also trying to optimize and so in some sense what socrates is saying it's taking away some of your freedom to optimize um by restricting its language but i also want to say that the the doctors compiler itself is a highly optimizing compiler and subject to its constraints it does a pretty good job maybe we'll talk about this a little bit more at the very end of the podcast

um but on on the whole it produces small circuits for what it supports cool and it's like a big project i think i think they're getting up on 30 000 lines of rust and a lot of that is is optimizing machinery so they've they've really done a good job there so you mentioned before that circum is a hardware description language but socrates i'm guessing isn't what kind of language than category would it fall under yeah the way i explain it to somebody who is who's new to computer science is i would say it's a programming language um but more formally it's it's a language in what we call the ram register model and and that means it's a language that that you could imagine executing on your computer

and and so this means that it executes in a way that refers to things like registers or variables and also has some access to memory in the case of socrates arrays that can be accessed at data dependent locations and and then in addition to being able to make variables and access memory it can it can perform computations just like a circuit can so it's sort of like a circuit plus plus right the ram register machine has circuits in it but also has ram and also has registers and and so socrates is sort of a move from this the circuit model which is what hardware description languages is capture to the ram register model um but

maybe now is a good time to say it's not a total transition so it starts to capture some things it captures the idea of memory in the form of arrays it captures the idea of ram in the form of variables but there are some things it doesn't capture and so one of those things that it doesn't capture is it doesn't capture this idea of branching of like an if statement where i look at some value and depending on what i find i either execute code a or i execute code b so inside the ram register model this is a conditional jump in an assembly and in some sense socrates doesn't have that fundamental thing it does have conditionals like if um something is true then a

otherwise b but it always evaluates both a and b um and even when you just like say that if you have like some intuition for programming you think how slow would my program be if i always explored all possibilities you can tell intuitively that there's some cost not having that yeah and then yeah that really does not does not help you with that but but there are other people who who did build high-level languages ram register languages that wanted to capture that as well and actually you know you can almost tell from like how technical this description is this starts to sound like an academic problem and and the first the first projects that that tried to capture this kind of control flow were academic projects so i think the the original one

is this compiler called pikin which is like kind of an interesting name [Laughter] it turns out it's like the name of some kind of like spicy pepper like okay random yeah yeah well but it gets better because the whole project like they had like other compilers in other languages too and there are other peppers um oh okay okay there was a set yeah yeah but the keane is like the the is the the most modern one and and so the the idea in bikini is they wanted to compile from c to a circuit and and in doing that they wanted to be able to capture things like branching and and also like arrays um as as as socrates did

um it's worth noting now that we're really violating the timeline because bikini actually is several years before socrates um but it was a sort of like a research project i would not recommend using it as an actual compiler but they had this this more ambitious goal of trying to capture branching now what about something like zinc the matter labs language that i don't know how finished that is but i know that like it exists i believe that you know i think alex came on the show oh by the way just in general to our audience i'm gonna put the links to anyone that we've mentioned i realize that if i say it every time it's just gonna be me saying it over and over again but check the show notes because i'll put those episodes but i think we had alex talking

about zinc so where would you place that does that fit with sircom does it fit somewhere further kind of like up the stack yeah i think fits quite a bit farther up the stack it's definitely in the realm of socrates and pikin right now it seems like the project is a bit in flux they they don't currently support producing proofs um and i've heard that they're they're trying to move to a new kind of poo system called plonk um so i think the exact details of what they'll support what they won't you know will they support arrays at data dependent locations will they support branching we'll have to see but um they're definitely going to be in the space of bikini and of socrates

um and they're not the only one in the space too so so another prominent project in this space is xj snark which is also an academic project although it's a little bit more polished you know they're trying to handle branching just just like bikinis and just like just like zinc might be but they they sunk a lot of time into trying to take specific cryptographic functionality like pedersen commitments or like hashes and and put them into the language as primitives that have very efficient implementations um and this is something that you can sort of do with any language but but it's a good idea and i i bet we'll see more of that in more languages as time goes on when you say that though is that something that other languages can then borrow

like would they be able to use that or because they've built themselves in a certain way they are unable to make use of that kind of efficient implementation that's a it's a good question i i think that almost any language could could play that trick it's pretty easy for any language to say okay i want to add a new built-in function or or some kind of new built-in abstraction and and even like the the techniques that you use to implement that abstraction efficiently with the the xjs snark uses a lot of those are our older techniques that were figured out when z cast was being built so it's not even like the techniques are super arcane um but the important thing to do here is to just integrate them in into a language so that people can write

most of their code in the language and then just have sort of the cryptographic primitives defer to this optimized implementation oh i think also one interesting shout out for xjsnark that's sort of unique about it is it has an implementation of large integers so this is kind of a cool thing that comes up when you're interacting with snarks there are equations over a finite field which means that you can do a lot of um sort of sort of arithmetic very easily um but once your numbers get too big to fit in the field you can't do that anymore and you have to really break out a lot of challenging techniques in order to handle it and currently xj snark is the best implementation of like 20 48 bit integers in that you can actually use as part of a

language and i think that this is something that other people should look at doing because if you want to capture certain kinds of cryptography like rsa based systems you need this big integer arithmetic and it's really not something you want to make users do inside the language because it's really tricky um and and because it has a clean abstraction so you can bring it into the language and still have this this nice abstraction okay so very recently there's been some work on a language called leo this is developed by by elio and at a higher level this is for targeting a sort of a zc based system but from the perspective of a language this is targeting circuits specifically rank one constraints just like everything that we've already talked about and in some sense i i think it

represents it's still in progress but it represents the best of many of these um so it implements data dependent control flow it implements some notion of arrays i don't think it's quite as feature complete as some of the academic projects in this space but it's a lot more polished than them and and i would definitely consider it like a part of the new generation of languages leo is that a one of these ram register languages or is that more of the hdl model it's it's totally ram register yeah okay um and i i would say actually its strongest selling point is that it implements this idea of data dependent control flow and branching and it does it with a higher level of polish than the research projects which were the

only previous things to do this they're not complete so leo still has a few a few things to fill in for sure noir is another upcoming project i don't know much about it but i'm excited it's being developed by the folks at aztec and and we'll see maybe you know hopefully it'll have kind of the same kind of quality that that leo has or that perhaps new iterations of zinc will have you've kind of talked through a lot of the languages that we have mentioned on the show but there's a few things that haven't been talked about yet one is starks so you kind of early on mentioned that starks are working at a different level but there is cairo which is i guess the language that starkware developed in order to interact with starks like where does that fit into this

entire kind of map so i think before so far we've been painting the stack as just kind of like two layers you got the language you got the proof system but the reality is that that not all the proof systems have the same interface so many of the proof systems that were developed early on have this interface of rank one constraints which is a particular way of writing finite field equations it has particular costs associated with it and starks are proof systems that are built for a slightly different way of writing finite field equations and and often the people who develop starks and talk about them describe their model as sort of ram register like and that you imagine applying the same

equations again and again and again and again in sequence so rather than having like a big set of equations you have a small set that gets repeated and so this gives them a slightly different interface and also it gives them a need for sort of new and different languages because they they have this different interface and so that's what cairo is so cairo is a language that is targeting this the stark model um and if you look at it it starts to look kind of like assembly languages that you might have seen in the past um so there's the notion of memory that it's pretty cheap to access there's notions of jumps and conditional jumps that are sort of baked in it's not a huge compilation problem to support them

i think really like cairo is sort of like almost like the gadget lib or the bellman of the stark world oh wow like the starting point in a way exactly yeah and i think that the people who advocate for starks think that they'll have an easier time getting higher level faster because of sort of this different model maybe that's true maybe it's not i think i think time will have to tell but but it is kind of exciting because it seems like we're seeing the beginning of the story for a sort of a new lineage of proof systems cool some of these languages as far as i understand have different models for storing memory and i guess this relates going back to that art like ram register versus hdl

circuit it has something to do with that but i we didn't really talk about it in the context of memory or at least i didn't understand it in that context is there some difference is there some way to to help us understand that yeah that's a great question like it seems like these languages sometimes adopt a different position with respect to memory what is what what is that difference and actually it sort of it relates to what we're going to talk about next which is the proof systems that underlie these languages as well so the first difference is that some languages almost all the ones that we've discussed are targeting the single finite field equation model the r1cs model and and that model has no memory okay so for them

memory is a compilation problem to be solved um and the languages some of them solve it well some of them solve it poorly or i shouldn't say poorly some of them solve it and some of them don't right some of them give you memory and compile it away and some of them don't now if you move to the stark model what they call air that's their circuit format it has sort of a notion of memory built in and so for them there's still some compilation questions related to memory like how exactly do you represent that to the programmer but it's not a compilation problem to be solved in the same kind of way it's fundamentally much easier to support because the proof system is helping them okay another question i have is last week's episode was all about arc

works we had pratushan we talked about that stack and we didn't just mention this in the last list of programming languages and we did on that show i also tried to ask him to place it in a map but i am curious where do we place it in this context where is arc works where is that work artworks here is from our perspective it's a proof system so it's what you do after you have a circuit um and it is actually sort of telling that inside arc works you have its own mini stack so even inside proof systems stacks within stacks and stacks and and so arc works in some sense in in some sense it's like a competitor to lib snark

and to the bellman implementation of the grot 16 proof system and to spartan into all the new proof systems that people are coming out with in some sense though its aim is to sort of be a unified implementation of all these different ideas so it's it's okay not really it's trying to be like an umbrella perhaps i would say yeah and that's what you mean by kind of a stack within a stack right where it's like it might have live snark within itself or bellman in itself exactly what's another thing that could be in it like would marlin fall in that would yeah fractal plonk redshift are those all the those are like as far as i know those are all like

circuit names i guess yeah all of those um in some sense to be clear they haven't implemented all of these but their observation is that a lot of these proof systems themselves like the distinct proof systems share common machinery and and it seems from the outside perspective that they're trying to collect all that machinery in one place and so i know they've implemented a proof system that we call gm17 and they have implemented grout 16 i don't think they've implemented fractal yet but and i don't think they've implemented planck either okay um but they've yeah they've done a great job of trying to unify as much infrastructure as possible in the proof system part of the zero knowledge stack i have one more question on on another

kind of project that we've heard a fair bit about which is like halo and i'm wondering does halo also fall into the r1cs world or is it like its own kind of thing on the side because i know that it does some pretty innovative things this is a little outside my area of expertise but to my knowledge so so halo is one example of of trying to build recursion into snarks and and this sort of changes how you can use them from the outside because you can you can um you know write one proof and then write another proof based on that and roll up their verification and this in some sense it's like a verification win in an asymptotic sense because you accumulate all the proofs

but but programming for it to my knowledge is is a similar challenge like um the each in each halo proof you you prove some single step and that step needs to be expressed as a circuit okay maybe we'll leave this aside or throw it out to the folks building halo to help us place this after the fact but so far i guess we've mostly been talking about except for maybe cairo we've been talking about these r1cs proof systems we're going to put arc works in there even though within arc works you can have some of the other ones but what are other proof systems that these languages may eventually be interacting with oh yeah that's a great question so i mean i guess like pick your favorite r1cs proof system like sonic

supersonic whatever right all of those are immediately in scope i think one interesting thing is that you could imagine taking these languages and getting them to produce circuits for slightly different proof systems as well and so there's a lot of work right now trying to take full advantage of plunk in some sense you can use plunk just like r1cs but that's not the best way that it can be used it supports other things as well and i think that that's something that we're going to see some development on over the course of the next few years another thing that you might imagine doing is trying to sort of heal this divide between the stack for r1cs and r1cs like systems and starks which are which are more like this ram

register model i bet that you could get a lot of mileage out of trying to build unified compilers or compiler infrastructure that that captures both of these models and and there's some challenges there but i would also expect us to see some development on that front over the course of perhaps a slightly longer time frame maybe three to five years now a topic that has come up a number of times in the show but also we did like a study club series on this polynomial commitments where does that concept fit into this language stack is it just being used throughout it is it something separate from it where does polynomial commitments fit in and what are they

so maybe just starting with what they are polynomial commitments are their own cryptographic primitive kind of like snarks or cryptographic primitive what they do is they allow someone to commit to a polynomial and then later on reveal its evaluation at various locations and and they fit into this stack you can kind of tell from their description which is very mathematical they belong in the proof system part of the stack so there are a primitive that are used inside of many proof systems so for example if you open up arcworks you'll find an interface for polynomial commitments and you'll even find multiple implementations of polynomial commitments that's one example of the common infrastructure that that project is trying to centralize so there's a number of proof systems

planck spartan i guess i think sonic as well that all are sort of almost entirely generic over their polynomial commitment and you can get different performance or different properties from them by substituting one polynomial commitment with another so like you said this is the very kind of mathy side of it but i'm wondering these proof systems are they connecting the mathiness to the computer hardware or are they connecting the mathiness to the higher level languages so in some sense their entry point is a set of equations over a field and and the the statement that i know a solution to them that's their entry point and they're

trying to connect that kind of statement with the hardware um on your computer so that your computer can check that kind of statement for you okay and also in doing that they're using a lot of very deep cryptography so in some sense they're connecting that statement your hardware and they're also connecting it to like complexity theory because like ultimately your hardware is going to run some verifier and that verifier is sound because of what we believe about the hardness of certain problems okay i think it's kind of exciting in that way like in some sense the proof systems they touch the highest levels of abstraction and they also touch the lowest levels of abstraction at the same time it's wild and it's so cool that this is all within this kind of specific cryptographic

field i wonder would you find the equivalent kind of like top to bottom stacks for other types of cryptography always that's a great question i i think the answer is increasingly yes and i believe the the reason that the answer is yes is that we're building more and more cryptography that operates over some kind of computation um so so we've been talking about zero knowledge proofs here the computation is is checking that some statement is true but multi-party computation is something that that even zero knowledge people interact with in the context of these ceremonies

that's also a multi-party computation is a piece of cryptography that's operating over a computation um and they have really a lot of the same problems that we have here similarly if you look at like witness encryption this is like a new branch of cryptography that's trying to build encryption systems around computation and they're very theoretical right now but i think if that work ever becomes practical there are going to be similar kinds of concerns there so i feel like we've done a pretty good job of mapping out a lot of these languages and concepts like in some sort of framework and as a disclaimer in case your languages

or your language was not mentioned or you're proven through with i'm apologies we we did our best and we'll always be adding to this list so do get in touch so that we remember it for the next time we do a mapping like this but i do have i have a question sort of for potentially people who want to get into working with this and that is like how do you actually evaluate all of these languages how do you choose what actually works for your particular application or your particular idea this is a great question um and i think that there are kind of two layers of questions you have to ask yourself the first question is where am i on the generality performance trade-off am i z cash am i going to write a single

circuit that everyone is going to use and really needs to do well or am i trying to build on top of zeeksy where i imagine lots of people are going to write their own circuits and so the first question is like which one of those am i and if i'm z cash i want a low level language that's going to allow me to say exactly what i want and really optimize and if i'm like zeeksie or i'm building on zxe that i want a high level language that's going to enable people who are non-experts to write circuits that they capture what they want i think most people are like zekesy i think that most people are not like zcash so then within the zekxy world within the model of i'm trying to enable lots of people to write circuits

there are a few things that you should ask yourself about a language i think generally you want languages that are in the ram register model not in the hardware description language model or the circuit model because more people understand the ram register model and then within the ram register model i think there's a number of test cases that you can use for seeing how well a language is capturing that model and these test cases they seem kind of arcane but they actually end up being very important they are can you mutate variables can you access arrays at data dependent locations and can i do data dependent conditionals where like only one side executes and those three things variables

conditionals and arrays basically capture the the hardest part of trying to to move from the ram register model to the circuit model and i think those are the sort of the strongest differentiators among languages so ideally you want to find a language that's going to give you all those things and this is maybe for people to evaluate because i mean we just mapped the languages that we know of today there's potentially going to be a lot of new ones coming online and so this is maybe a bit of a framework to help them navigate that with the languages that we mentioned this is kind of a side note and actually something i should throw over to the circom team but i wonder like would they like given that they are more of the circuit model is it possible for them to

also create something that would interact with the ram register model like could they create something on top of themselves i think they could yeah for sure from from my perspective as a language designer i don't necessarily see the case of going through circom instead of like just going directly to a circuit from this higher level language um okay but i could be i could be wrong about that and and regardless um that team has a lot of knowledge about implementing languages and i'm sure that if they did a ram letters for language it would be a good one cool maybe that's a little bit of a wish list jordy if you're listening um cool i'm trying to think is there any other differentiators that we should touch on uh for people to think about when

they're analyzing these languages for their own projects i i think there are some other things too and these are things that i think you would ask whether you are programming snarks or whether you're programming your computer which is how good is the compiler like do i have good error messages do i have good tooling in in this in the snark world that looks like you know can i produce ethereum smart contracts that valid like is it easy for me to go from a program in this language to an ethereum smart contract that validates proofs um for the circuit so i think these questions are on tooling are also really important and they're the reason that things like bikini or xj snark the academic research projects are it's not like they're bad projects but they fall a little bit short on that

frontier yeah got it is that sort of like you need to have an ecosystem does it have something to do with like the number of contributors not only the amount of tools because like the obviously i'm assuming the more contributors the more just activity generally i think so yeah yeah and this is all about can you get people to to invest and to build those tools yeah and those problems are are really really really challenging um actually like i think that you know on on the global scale these questions around ecosystem are actually what determine the rise and fall of languages um really you want the compiler to be kind of a detail that you don't have to worry about too much so actually maybe this takes me into something that i wanted to bring up which is like

i we mentioned already that there are these hard compilation problems that these languages have to solve and and you know data dependent array accesses conditionals variables and it's kind of a shame that in the current state of affairs languages all try to tackle these on their own and ultimately they choose to tackle some of them and not to tackle others and you end up with sort of a patchwork landscape um where you have to ask that question like does this language support branching because it might just not because they have finite time and it's a hard thing to do and so one thing that i've been doing recently with some friends of mine is is making the case for a kind of an llvm-esque general infrastructure for supporting

these languages that can handle these hard compilation cases automatically so we've we call this project cersei and the observation is that variables are hard branching is hard memory is hard there are other hard things but these things are hard in a way that doesn't depend on the syntax of your language it doesn't depend on exactly what types you support it doesn't depend on pretty much everything and so it's possible to implement that in the same way that arc works tries to centralize infrastructure reproof systems it's possible to centralize infrastructure for compilation as well and that's the goal of this project we actually got a chance to do an entire like zk study club on cersei which i'll add a link to

for people to explore but given that you're here on the show is there anything more that you want to share with us about that maybe like the stage of the project what you hope it becomes yeah i think so the state of cersei right now is that we we sort of did a prototype of it and we are in the progress of porting the the project to rest and sort of cleaning it up as we do that now we have a much better understanding of what it's supposed to do um and that's actually coming along really well um so our sort of uh first checkpoint is going to be supporting socrates through our conflation infrastructure and we're getting pretty close to that i think that

what that project could mean to the community is it could be a tool for all these developers that are creating new languages and new compilers so if you're listening to this and you've been tasked by your firm or just as a hobby project you're trying to construct some kind of language totally come talk to us um we it seems like we have something that can make that job a lot easier and also like we're in the progress like i said of porting it which means that there's a chance to chip in here and be sort of one of the founding people to to get this infrastructure into a super productive and effective state so i want to say a big thank you alex for coming on the show and helping us navigate all of these amazing exciting new languages old languages how they

interact with one another i honestly feel like what we talked about today it's something that i've been kind of unofficially trying to do myself for a while like to understand and place where these things live i think this has been a really great run through to help better formalize that in my mind um so yeah big thank you oh thank you for having me it's uh i i think i also really appreciate just how rich this landscape is and it's uh it's a lot of fun to try to map it out i hope you get to come back sometime and and share maybe some updates as a lot of these things come online yeah that would be a lot of fun cool so to our listeners thanks for listening