ZKPodcast: Zokrates with Jacob Eberhardt

Transcript

[Music] welcome to zero knowledge a podcast where we explore the latest in blockchain technology and the decentralized web the show is hosted by me Anna and me Fredrik [Music] in this episode we'll sit down with Jacob Abraham the Socrates team to talk about the toolkit that they're building for zero knowledge proof welcome Jacob to this episode of zero knowledge

podcast where hopefully we can dig in to a little bit of Socrates and hello Anna as well hello hey so why don't we dig into your background a little bit immediately and how did you get into working on this you know how did you get into blockchain so during my studies I initially studied business engineering and only had a focus on computer science but then I get got more and more interested in computer science and focused on that as much as possible in my studies and then as I graduated and said I want to learn even more and focus more in computer science I started

working in a distributed systems research group where I'm also still working but back at the time there was only Bitcoin and not much else going on in the blockchain space so I did what I was interested in back then and that was distributed database systems highly replicated highly available no sequel systems and I thought about data types that help scalability and and conflict resolution in that context so then when I felt like this topic was covered and Ethier and slowly came up I became super interested in the theorem just because it was like a whole new world opening up the idea that you could have economic

incentives being used as a mechanism and computer system design to enable new types of protocols and to have one global state machine and so I found that super fascinating and also it fit quite well with my background in distributed databases I would say because you can't always say that but generally blockchains are still distributed databases in a way just with very high replication factors and so it fit quite well and then I went all in on blockchains and it and a theorem also in my research and that's how I ended up studying scalability and privacy

blockchains privacy problems in blockchain and that's how I ended up looking deep in blockchains and soon all this proves as a way to tackle these issues so you're still a researcher and PhD student at a billion tell us a little bit about some of the work that's come out of that tell us a little bit about Socrates okay so when I started looking at add ways how blockchains could scale and also have better privacy properties it became apparent that the main problem is the full replication that every computation is repeated on every single node in a network and that every node stores every

data item and if you look at transactions and block chains from a very high-level perspective you could say it essentially has two steps I would say one is to load and persist state and the second is to compute state transitions and based on that abstraction I started looking at could you off chain either of those parts and as it turned out off chaining storage is quite difficult because as soon as you put data to an external system you can still enter integrity for example using hash pointers but it's very hard to guarantee data availability because then the data may not be available because

the outside storage system becomes unavailable so the storage route will we did some experimentation and research there is useful in particular use cases but not as general-purpose I would say in comparison computations like computing the state transitions can be off chained very well in my opinion and then block chains Oh what they're very good at doing I would say and that's storing data keeping it highly available so the system can always make progress we refer to that as life news and then we compute the actual state transition somewhere else and then

need to make sure that it was computed correctly where we send it so Socrates is starting as an off chain computation project exactly so that was the main idea and then coming from that application essentially I started looking at different approaches of how you could do that off chaining in a sensible way because if you do it naively you reintroduce trust to the system you would expect that the the off chain computation is done by some third party node and then when the result is written back to the blockchain it cannot be used because the third party node could have lied so what we need to do is make sure that there is a verify step that's executed on chain or some other

mechanism that ensures correctness and that's a key property for off chaining computations that correctness is always given under the weakest trust assumptions possible and this is where sort of zero knowledge proof scum in exactly so certain knowledge proves there an established field of cryptographic research I would say and they're not very young but there's more recent results for example see case narc construction that made it practical that made the proof sizes small and that made verification cheap and that made it possible to consider it for such a blockchain application I want to get

back into that trust factor a little bit but we can we can get back to that later because in as people may or may not know who's especially from our Howard episode Zacchaeus narcs has this bit of trusted setup so I want to know how you deal with that but how would you define Socrates just like what's the elevator pitch can you do an elevator pitch for such a complicated project actually one should always have an elevator okay I assume I'm not very well prepared then but I'll try so Socrates is essentially a set of tools plus a language which enables developers to more conveniently construct sir knowledge proves and verify them on the

blockchain because the low-level cryptography is there it's there in theory and as Howard explains where well there's also lip snark and there's bellman which are low-level libraries that allow you to create these proves and verify such proves but the problem is if we want to use this in the blockchain context we need a higher level abstraction in my opinion so it actually becomes available to developers and can be used by non crypto experts and that was kind of the goal for the project initially to create another abstraction that wraps the cryptographic details and low-level things in a more

convenient way and then also like enables optimizations in the process for example so that regular developers as smart contract developers for example will have access to these kinds of tools it's very cool and I when I did my little bit of research before this episode I actually realized that that I had misunderstood or were sort of partly understood what Socrates is I thought it was just the blockchain parts where it's just proof verification on ethereum but it's actually much more than that can you explain like a little bit you mentioned these pieces like what is the

data flow in the system okay so yeah it's it's more than that and I would say there is probably several key components and I would just start from the perspective that a developer has and then we can cover the components so a developer would first need to specify the computation he wants to prove that means he wants to show that he executed computation correctly and also he wants to be able to use private information in the process that means use some data that does not become public as the computation is executed essentially so he would first start writing high-level socrates code and there is a

domain-specific language that is specifically tailored to make it easy to specify computations in a natural way but also in a way that efficiently translates to the cryptographic low-level primitives so we can still efficiently construct proves in the end that's why we choose a domain-specific language and not just went with some arbitrary high level language that's already established and then after a developer writes that code it goes to the Socrates compiler which translates it to a provable abstraction that means generally with reference to the episode

you that without with Howard to an arithmetic circuit or a rank bond constraint system which is another low level abstraction but it's quite close in expressiveness and then as you have that circuit there's two things that need to happen for that specific circuit as you already mentioned we need to do the trusted set up and we do not support any highly involved set up phase that is decentralized or distributed in any way at the moment but it's pluggable so secure multi-party computations if they should be used for that trusted set up

as an alternative or lower trust thing could be plugged in when you say when you say this more complicated one is that like woodsey caches trust the set up like this yeah so what we offer out of the box is just a local trusted set up so that means for the circuit you generated by compiling high level code you then receive a proving key and a verification key and you can use those but if you actually want to be able to convince a third party of the things you've proven there should be that third party would either need to trust you or you should do a better more complex distributed set up phase so the trust

assumption is weaker with your background and you know distributive computing and how you got into the blockchain space did use like which ended the did you start in was this always the vision to have this whole tool set or did you start with like oh we're just we're verifying on if there am or did you start with we're gonna do a high level language it generally proves so initially there was that idea of we could use these verifiable computation schemes that are non interactive and give short proves that are cheaply verifiable just to scale block chains and to give better privacy properties and since a theorem back then

was like the the main network that was actually ready to use and available it was the obvious choice to experiment with so the goal was to do this for a theorem and today we still mainly focus a theorem with our smart contract verification smart contract generation which will probably go to in a minute but the idea was rather implementing this idea and building only what is needed and the the goal was never to build a domain-specific language in the first place but just to realize that

idea in some sensible way and proof verification was not even available in the theorem so back then Christiaan right wizna who i often sent with implemented pre-compose to pre-compiled contracts that were required for seek a snark verification and i in parallel together with students developed the first Socrates version that then enabled to write provable code and actually verified on these employ change so that's where it all came together and that's why there is still that tight link with he theorem so I feel like in your description of the components I feel like we got to the

part about trusted set up but maybe we can continue from there what's what else is a developer gonna see so the compilation gives you that arithmetic circuit or in other words a set of constraints and what you essentially prove when you prove that you actually executed a program correctly is that you know a satisfying variable assignment for the program so it fulfills these constraints and that's why as a step before you can generate the proof actually you first have to execute the program and in this context that means finding a variable assignment so in the

end all the constraints are fulfilled because what you prove overall is that you know a satisfying variable assignment for the program but you do not expose all these variables and that's a certain knowledge aspect of it and then the verifier checks whether you knew a satisfying variable assignment and that in the end equals executing the program correctly where does the verifier live in this is the verifier on chain is a verifier in the smart contract in the in the general idea of their knowledge proves there is no specific answer to this to verify I can live anywhere and can be anyone but in Socrates as it's specifically tailored for blockchain applications the

verifier is a smart contract that lives on the blockchain and as soon as it receives the proof it verifies the proof and in case that verification was successful it stores the result and also stores in the history of course that the verification was successful so then other parties can actually rely on the outputs of the computation you mentioned something that I've never really thought about with zero knowledge proof that it's sort of a constraint solving problem yeah and I mean I've written like constraint satisfaction systems before and it's yeah I never really thought about it that way it makes sense like

it's he clicked in my mind like it well how their knowledge proofs actually kind of work but yeah so to recap the developer story sort of as you write your code in this high-level language that you've made it sort of looks like Python by the way it was that the inspiration or yeah so the initial inspiration was actually a block entry Vitalik did where he when the discussion came up of how house their knowledge proofs could be incorporated in a theorem and how they work he started and just gave a very very simple example of how to prove a simple arithmetic statement in sir knowledge and I think I'm not 100% sure he even provided a bit

of Python code and that's why he the syntax was Python like and then we thought about it and I think it's a nice basis for DSL design and that's just why we went with it so you you're at your code you generate like you send this off to the compiler it and then you generate the prover and verification key and this trusted set up then you can generate your proof by running this program you submit the proof on chain and if it's verified on chain yeah so there's one thing from user perspective that finding a solution for the constraint system and

then proving that solution it's two separate steps but in the end it boils down to exactly what you said what are those or resource requirements to generate a proof like do you need a beefy machine like a massive server to run it or like it obviously depends on what what program you're right but for something semi normal this is very very hard to say because there's not a single metric you can pinpoint it down to if you look at the constraint system what's relevant is the number of variables in your program and the number of constraints but as you display that this constraint system in a matrix form then the density of the metrics also becomes relevant so

it's very hard just for a given program to say how expensive it's going to be generally I would say memory needs to be big and you need access to a lot of memory optimally more than you usually have on your laptop because if you don't have that you're using swap and then proof generation becomes very very slow so yeah memory is usually a bottleneck and that's where very large circuits start to fail them going back to this trusted set up thing I just wanted to touch on this a little bit because like you mentioned there's you can do a multi-party computation style set up that see cache did for instance but the

default in Socrates is just a local generation so what is the use case then of the of just a local one is it in like in more closed environments where you already have some implicit trust between the sort of def maker and the user or is it in in private you know consortium block chains or what do you imagine to be honest it's not because we make an assumption of what the proper use cases would be but we rather say people need to find out what their trust assumptions trust requirements are for their specific circuit and then incorporate the setup that is yes efficient or desirable I think we could in the future

support that programmatically like provide more tools so people can conveniently do distributed setups we started experimenting with that and also doing a non chained multi-party computation a prototype so it could potentially simply be that I want to have a smart contract that uses CK snarks and NSA okay now I want to do a set up for this contract and then you have an on chain coordinator that coordinates that set up and gets contributions from all parties that want to be involved but the problem is that you cannot rely on the pure number of participants in that set up because it's civil attacks can easily

happen so the same physical entity participates several times so in the end it boils down to if I do not want to trust at all I need to participate in the setup and that can be realized in several ways and depends a lot on the specific use case so you mentioned just before that it compiles into a circuit but what circuit is that exactly what is this based on the circuit is actually in a format it's called rank one constraint systems and it's not strictly a circuit but it's equally expressive and it's just a way to express a set of

constraints so that you can then use the zero knowledge we have variants that are provided by a lower level library such as live snark for example to generate your proves that's so does lib snark have like native support to take these rank 1 systems yeah lip snark enables you to use a translation from rank 1 constraint system to quadratic arithmetic programs and these quadratic arithmetic programs then the abstraction the proofs are actually performed with but it's a common abstraction I would say an interoperability discussions for circuit

also often yeah include or propose our one CS as one option for example for circuit specifications so it's a standard format in a way but the problem with rank one constraint systems is that you use what I call witness derive ability so what you have in the high-level language is you have an impressive way of writing your code and with that it becomes clear how you arrived one variables value from another variable if you translate that into a rank one constraint system it's only constraints it's essentially assertions

and in that process the information of how one variable can be generated or computed from other variables gets lost so I would say the rank one constraint system is the sufficient abstraction to then build proves on but it's not a good interoperability format because when you get that system it's extremely extremely difficult it's an np-hard problem to find a satisfying variable assignment and that's why I think we need a better interoperability format because we have that information in our high-level language this is something we've talked about before on the podcast of standardizing Howard has mentioned several times there is no standard way

to write these circuits so there's no interoperability between libraries and stuff it's that's anything I didn't know that this rank one constraint system was like even a part of the question here so I think that's an interesting aspect that you know pros and cons of having that be the interoperability as well so just recently we sat down with Benedict once from who's the co-author of bulletproof and I've been a little curious about where bulletproof could fit in with Socrates or if it would ever fit in with Socrates so bulletproof so a very intriguing proposal I would say it has a very cool property that they do not require trusted setup and it's always limiting potential use cases

causing overhead cost for setup procedures and also yeah it it requires trust which is usually very bad thing in the context of block chains so that's why a bulletproof saw very cool they were initially designed for range proofs but they can also be used to prove statements that are expressed as arithmetic circuits so it's essentially the same abstraction that ckase norwich that we use are also based on so theoretically we could simply use the same compile do the same compilation steps and just use a bulletproof implementation in the back end instead of lip snark to then be

able to generate bullet proves the problem here I would say is that the verification step in bullet proves has linear complexity with circuit gates and that's why the on chain verification where it quickly becomes impractical and and that's why it's viable and quite cool for small circuits but as your circuits become big it becomes super expensive to verify also ckase narcs they are extremely efficient they have improved size off with across 16 construction and a standard curve 127 bytes so it's very very small bullet

proves they're still quite good especially like compared to CK stars or other constructions that do not require trusted setup but they have a few kilobytes in size so I think we are compatible with bulletproof Stu questions rather our bullet proves the right cryptographic tool to do off chaining of more complex computations they certainly are the right tool for range rules and small circuits but if you want to do complex stuff ckase norwich seem to be unbeatable verification is of constant cost and it does not matter how complex the often

computation you want to prove is for the verification and that's different with snorerx with bulletproof and that's why ckase narcs are still very very attractive and practical although they have that setup issue I want to ask a little bit further on that so I'm curious can you already can Socrates already work with bulletproof if if one wanted to like is it possible and are there other zero-knowledge proving systems that could also be used with Socrates there are multiple other proposals like Leggero or hyrax that are different cryptographically construct I always have a hard time saying it can be used with because they haven't

implemented it so from a theoretical perspective it could be used with CK starts for example it's a bit different because they modeled their computations differently it's not arithmetic circuits that translate to quadratic arithmetic programs but to polynomials of higher decrease so because the underlying cryptography works a bit differently the translation is not quite that straightforward or comes with some inefficiencies if you were to do it but bullet proves to be honest should be very straightforward to integrate it would be cool to have like in some

distant future a toolbox like Socrates that basically analyzes the size of your program and if it's something very small it automatically picks bullet proof if it's something medium it sort of oh hey you need a trusted setup for this because I'm gonna use you know lip snark or like if it's a massive program or you put in some constraint that it has to have no trusted setup it picks darks or whatever yeah that's a very good idea we should we should work on that it's like such a yeah you're predicting the future Frederick I have another question about like different systems so you you mentioned before like a little while ago that you had built it around the EVM and aetherium because that was coming out

around the same time is very exciting could this could Socrates also work with other protocols the only part that is specific here blockchain specific is the verification smart contract so the logic that checks that the prove is correct essentially and this aspect of Socrates is quite small it's just a smart contract template and we fill in the verification key and add as a smart contract operation and the computational steps that are needed to verify proves so it could done for any plot chain that

supports sufficiently complex operations and it also would need to support these operations in a way that is efficient enough and that's why theorem uses the pre compiles for the underlying operations so you can actually do the verification of proofs within one block interval and optimally many many verifications within one block interval there is room for improvement our current implementation uses the Pinocchio CK snark which has proof sizes slightly under 300 bytes for the curve we use but we couldn't move to more efficient snark

and we're currently experimenting with that that reduces it to 127 bytes as I mentioned earlier also the pre-compile could just become cheaper because client implementations become better and that is very blockchain specific so that could be totally different for a different blockchain so it could be that another plot chain will be able to verify many more proves within one block for example also we could but the problem is that a theorem does not support it and the current version move to a better elliptic curve that allows

other cryptographic primitives to be used and is overall more efficient and this is the the argument behind was in block chains right and like II was him and all this stuff is that you can you can write all these curves deploy them by yourself it doesn't have to be a built-in contract or precompiled yeah exactly if we had wasn't we and this was efficient then it would be much easier to experiment with new cryptographic primitives it would not require a hard fork and everybody could just choose the curve he's most comfortable with because there's oftentimes also a trade-off between what's the perceived security of a curve and how long has it been around and not

shown to be vulnerable and efficiency of the operations so before we move into our next little section that I we want to talk about which is how do you learn all this stuff I wanted to just slightly personal question all more or less all of Socrates is written in rust why did you pick rust oh that's a good question like we had to do it in some language and when when you're researching you always try to maximize what you learn on the way so we thought we may use that very cool new language that has zero cost abstractions very good type system and just find out whether it worked for

us and it has shown to work very well for us so I'm quite happy with the choice it's quite quite cool and the good thing is if we at some point move to Wasson then we can compile from rust to wasn't very easily so it will also help us make required changes to be future-proof more easily so our listeners don't know this but Frederic is smiling a lot right now as you described that so obviously this is not a super simple project and I think this interview we've gone pretty deep into it are there places that people can already find some of this material do you have talks do you have slides like where

would you direct people if they want to like see this in a like a little bit of a bigger picture so there's multiple resources there is our github repository that includes some samples and a very pre setup guide but I think we could do a better job there onboarding people but that's something we're actively working on there are multiple talks that are available on YouTube I think so I presented Socrates initially at the theorem DEFCON 3 and Cancun so that talks available there's also talk from the theorem community conference in Paris and there's also I think a presentation from a meet-up in Berlin which was done together with

true--but nice so I think there should be some videos out there that explain that stuff in another way and that also have some slides and pictures also my github account in notes you can find these presentations so if people would like to check out something more visual that's where to find it cool I think we're also going to put at least a link to that in our show notes but probably some of these other ones as well all most importantly though there's a research paper on Socrates which was just recently presented at the attribute blockchain conference in Canada and actually won best paper award so I

suggest you check that out congratulations Thanks so I just wanted to ask as well because like in a more general sense you're still involved with the university and maybe you're dealing with students and people trying to get into this space what would your recommendations be for like if I'm I know computer science or no programming I want to know zero knowledge proof so where do I start and how do I actually get up to speed on this stuff so I think what you first need to do is to answer the question for yourself whether you can live with not understanding how it works mathematically in depth and if you can then it's much simpler if you can't like I did you have to dig into the

papers and read up on that stuff and probably learn a bit more about cryptography and proof systems in the process so I think the Pinocchio paper is a good point to start because it's quite accessible and already describes a mapping from arithmetic circuits to proves and then generally the work of Eli Ben Sasson is very very cool and I recommend you check that out if you're really interested in theory another approach would be to just start playing around with lips norik or a bellman which are the libraries that allow you to compose approvable

arithmetic circuits on a very low level although it's not super useable in my opinion or at least requires quite some expertise because it's not straightforward of how you would express a computation in an arithmetic circuit in the first place but that would also be an option and then the third option is looking at domain-specific languages like Socrates and trying to understand how they work internally gaining insights on that translation process because I think if you understand how you go from a high-level program to approval abstraction and then just look at that proof system as a black box and just study its properties a bit it can get you quite far and you can

meaningfully contribute to the further development without having a very strong mathematical background so you were telling me that you actually are working on or maybe have submitted a paper about the different approaches to off chain computation can you maybe just briefly give a little little teaser about what you what you have there yeah okay so um very briefly from a high-level perspective we try to put together a paper that describes the different approaches to Australian computations in general so not only the verifiable computation schemes we talked about now as one options but also other promising

approaches that are currently researched and also not so promising approaches maybe just to get an overview of what's out there what the possibilities are and what the trade-offs is so maybe just mentioned a few other high-level ideas or categories that yeah that can be used in the context of off training so one would be enclaves based systems that rely on trusted execution environments implemented in hardware to execute code off the blockchain in an in clay for example in an Intel SGX system and that can also be privacy-preserving

because data does not leak and can be sent to that in clave in an encrypted way and then the result can be published to the blockchain together with an attestation that involves several trust assumptions regarding Intel's as Jack's attestation service and but is it is one option and it's actively being researched and also built by enigma for example who initially proposed to secure multi-party computation protocol but then shifted over to trusted execution environments just because it's more practical today and I don't think it's completely unreasonable to explore that space and also akedan which is a

proposal by Oasis labs they also try to use trusted execution environments and published a paper on how to best do that so that's one approach another one I just briefly touched already are secure multi-party computations where you have the idea that instead of executing some function on chain in a way that the yeah the the data becomes public that's a more fun computation you use a network of nodes and distribute the data to the these nodes in a way that no node knows more than a meaningless share of the

overall data they then do computation on top of that data and intriguing property of that system is that if you then after that computation that was done independently but every single node if recombine it in the end you get the meaningful result which equals the application of the function to the original secret data if you then publish that on the blockchain and make sure that correctness is given and for that you can use a public audit trail that's proposed by some secure multi-party computation protocols then you can also have a way to do privacy preserving often computations however it's not very practical I have to say because these

multi-party computation protocols as we have tomb at the moment they're not very fast what's an example I mean is there any projects that we might know that are doing this I'm only aware of enigma who proposed that initially but then I think they're still interested in it and doing it but I'm not sure whether how active that is it also sounds like a lot of these different solutions or different ways to do often computation or sort of use case dependence like you wouldn't you can't do a multi-party computation for like zipping a file because you need all of the data to be able to analyze it to create the most optimal compression

oh yeah depending on which compression algorithm you use but whatever but but on the other hand something like a MapReduce where you split all the data into pairs and like send two pairs to a person and then they computes this and then you send the next two pairs in a sort of binary tree structure that's very easy to distribute I mean that's that sort of like known exactly and and we wondered how these different approaches compare what the properties are what the on chain verification complexity is what the often computation complexity is whether they're post quantum secure whether they support privacy features what the security assumptions underlying these systems are so that's why we try

to compose a big picture overview of these approaches another approach for example would be incentive based off trend computations as implemented or proposed by attribute for example where you have an economic security assumption essentially and just assumed that people will meaningfully contribute to the network as long as there's no economic incentive to do so and by incentivizing properly you can make sure that false results published to the blockchain will always be challenged and eventually the correct result will be on the blockchain so Fredrik you know you had just earlier said it would be really cool to have

this tool box that would like automatically choose different zero-knowledge proving systems when it comes to off chain computation like would there also be like do you think that's kind of the future that there'll be like a meta system that will basically start choosing the ideal one or do you think that every protocol would be tied to like one preferred off chain well it's it's the use cases are a lot more dependent on what you're actually trying to compute and it's a lot it's a lot larger system in a way like if it I mean for some things maybe but in some cases your entire application is this way to do the off chain computation so might be hard to like abstract like properly abstract

because like you can't just write a general program that you know from that derive some information on how it should be distributed to my knowledge it at least maybe someone comes up with such a structure but it's a lot more complicated question also if I may add to this there's very different security assumptions for all these approaches and I think different networks different players participants feel comfortable with different security assumptions a cryptographer looks totally yeah differently at things then a person just setting up their private network where they control their hardware so I think yeah time will tell what people will

accept and whatnot but I don't expect there to be one single answer so I also don't expect that it's necessarily agar if mcclee decidable which off chaining pattern would be optimal for a given use case so we're talking about this kind of space right in between you know industry these different applications of option computation patterns and like tool boxes that people actually use for applications but it's also very academic obviously it's it's a research project and like you analyse these industry applications as a form of academic research area how do you feel like the industry and academic spaces compare like what are their motivations how do

they move and oh that's a good question because I think in the context of blockchains they move closer together than they've ever done before and I think that because block chains are not they don't have trade up business models you could say so the financing models for blockchain related projects changed and also there's a lot of research involved at every single blockchain project at the moment just because there are these scalability limitations there is no perfect solution to privacy at the moment so every single project tries to yeah link with academia talk to academia

also do research within their industry project so I think that's why both spaces moved close together also academics are very happy that their Theory finally sees applications that like that proof systems are actually used in a meaningful way now and so I think it's it's quite cool momentum in the space at the moment that makes both spaces move closer together and also helps academia to yeah make the point that their contributions are more meaningful as it may seem sometimes we

heard this from Howard as well that it's not only that it's cold that the theory gets you know used but it that it gets used so quickly that you know a paper can be published in a couple of months later there's some proof of concept implementation somewhere by someone yeah for example Howard's physics system they just published to scale computations that would work super well with Socrates because it would just allow improve generation to be sped up a lot and that's one of the things or one of the contact points that you just mentioned where it just fits where well together and it feels like it was just the missing piece and the puzzle and then it gets adopted super

quickly also there's a big pull from industry I would say there is funding of research project in a way that we've not seen traditionally there's corporations between industry and academia in a way that we've not seen before so yeah that's quite cool it's interesting Benedict also we also had that conversation the one thing he added to this was we were talking a little bit about naming and how like these academic concepts are getting named in much cooler ways and this seems to and Socrates I think falls into that bulletproof disick these are cool compared to what they would have originally have been called which were

like these long very technical names of projects and I don't I I think this might be a good kind of ending point for this podcast but where did the name come from Socrates oh yeah just one thing I may I might want to add so these names are cool but they're a bit difficult for academic papers so that's why we now need subtitles okay and also I like that Benedict especially in the acknowledgment put the person that came up with the name so where did Socrates come from I don't know I was talking to one of my students back then and we felt like we need a better name because we had that project and on github it was called verifiable

all chain computation something okay and then Christian right wizna asked me to present at the meetup in like three or four hours and then we were like okay I think we need a name what would be suitable and then we came up with the quote by the philosophers Socrates it goes something like I know that I know nothing and then we thought we briefly moved to I know that I show nothing and we made that Socrates to like hint at the certain knowledge property and then we felt this is quite yeah like a cringe moment we

can't actually say that this is where it came from so we just went with Socrates and never told anyone where I love that that's amazing love that you think it's cringe-worthy that's hilarious never to be spoken again although it's obvious that Socrates is Socrates somehow but that's really cool this was so much fun to explore Socrates with you and yeah I just wanted to say thanks so much for kind of taking us in to this relatively complicated project that you have and I really hope that our listeners got something out of this I think as we mentioned before it's probably a good one too if you're really

into this to go check out a lot of the other resources that are out there specifically like graphs and sort of images to show those components I know that we've looked at that and that's been super helpful yeah so thanks so much for coming yeah thank you very much for having me wasn't honored to be on your podcast and to our listeners thanks for listening thanks for listening you [Music]