ZK10: Juvix: A language for intent-centric and declarative decentralized applications

Transcript

foreign [Music] hello everyone um I'm very excited to present uh this Workshop about geovix it's uh it's a really interesting project it has many ideas it has evolved during this last year my name is Jonathan kudis and I also prepared this with Paul Cadman which unfortunately couldn't come today got sick and all right let me try to say a few of the goals that I have for this talk

I want you to understand what is juviks why we are building this new programming language for anoma and I believe we can use juviks also for or different purposes and in particular since we are here in CK Summit I would like to just present a little bit about the compiler infrastructure to support serial knowledge proofs and my main objective today is that you can try ux yourself on your machine so I hope you can open your laptops and try it with me uh all the exercises that we prepare for you

uh all right before delve into the specifics of the talk I believe it's important to just mention the people that is behind this project we are a group of five we are mostly just mathematicians and or computer scientists with a background in formal verification and type Theory this is my team is Paul Cadman Jonathan it's my name and Lucas shaiker and arten goodef and John Manson the team so in very short terms juvik sees this high level language that we have for writing animal applications

we are designing this language to have privacy preserving uh decentralized applications and I would like to give some context will justify why we are creating this new programming language so anoma this is the definition of anoma it's an intern-centric architecture for decentralized counterpart Discovery solving information flow control and atomic multi-chains settlement right and I just said that jurix is this programming language that you are going to use or that you can use to write applications for a Noma so for uh improve the understanding of

anoma here I prepared this so anoma is based on the concept of intent so this is really Central It's A Primitive in this context and intent is basically just a message that Express how you want the the state change right so it's a high level description it's a program that encodes your preference about how the state's Gonna Change so um we have here this is a simple example of two paria change

right we have three actors in this we have Alice and Bob and Alice has the intent uh he wants to get one unit of dolphin and is willing to trade either one unit of item a or it or two units of Item B that's Alice and we have Bob who has also uh desired to trade one unit of dolphin for and and it can give um sorry it can trade one dolphin for one unit of a right that's uh the preference and we have in a normal component that is called Tiger Tiger is a framework for

children's actions but is the component in a Noma that is in charge of dealing with this intense and there is another concept that we have in tiger that is called personal transaction so before to submit any transaction to the blockchain we need to prepare it and the way uh that we need to do that is to create partial transactions and once you encode that in something that tiger can't handle we put this into a gossip pool where all the intents go and there is another component in a Noma that is the infant solving so we have solvers and solvers are basically just algorithms or uh that can be users as

well or just other programs and these solvers they can unfold information about the um about this about this intents about this partial transaction and there are some other specifics that you can use in order to get a match in between the preference of Alice and Bob right and once you find a matching then you can uh get the finalized transaction and submit that uh to anoma or of course I'm oversimplifying many details here if you have any questions regarding the cryptography I have here my colleague Alberto who is the person that can uh

that is designed in Taiga as well and yeah all this concept of intense me uh with my team we are just uh developing the programming language so the programming language looks like what you have on the right uh so we have an API for tiger and you should encode every intent in what we have modules here right so I don't really expect you fully understand old encoding here but as I said an intent you need to encode it as a partial transaction for example Alice I said that is willing to trade

one unit of a or two units of B for one dolphin so in Taiga you have these two um to to pair components of a person transaction so you said um what are you gonna consume and what is going to be um available later that's the created pair right so you can see here that you have one unit of a or two units of B right and we have another encoding for the Alison 10 so this part

gets a little bit more trickier because you need to uh you need to encode the logic which are just the conditions for your transaction to be valid right so you can express this uh using this um predicate which is just a function that gets value into bull and um and there is this encoding by the way I'm just taking this example from the documentation so you can just go to docs.jiviks.org and just uh follow this all right and there is other components and also if you're interested how

exactly the transaction life cycle is we included like a client server sequence diagram for you to understand this is the long term this is like the this is like the main goal uh for juviks is to be the language thing which you can write this intents to able to create these transactions on the animal blockchain basically right okay um let me go back to my so that's the that's the reason why we're creating a new programming

language uh and it's important because I know my itself can be seen as a operated system right where the Primitive notion is the intent and as any other operating system there is a notionable computation which is not the same as the computer that we're running this uh it's lights so uh those details are what makes a special uvx because we are targeting a different model of computation but the specifics I'm not going to go into details anoma and juvex are these two projects that are on heavy development and we are

figuring out all the details about how to make a the things work right um yeah so these are our three main goals for juviks and we plan to be uh a language jointly with the compiler of yeah for the for the for a normal basically right yeah these are our main goals however uh while developing the language we are not really limited to anoma we can um we are actually reaching the point where juvex can be just a general

purpose programming language and as I said in the beginning we have a pipeline that compiles to server knowledge proof which I believe is what you are here so our compiler starts with a file that is written in jubix this is the extension and we perform different static analysis of course we need to parse the file and we have a type checker and we have this juvex core which is the main core language is just anti-blum the calculus with some extensions and some optional typing and for this intermediate representation we have back-ends we have native binary

um output we can deploy to wasm we have this in-house compiler that are called vampire and Gap and the purpose of these two backends is to produce uh serenodesproof right um so I was checking on the on the lack of CK Sumit and I found that there are some talks about vampire so you can check it out online you take juviks and you generate a vampire code and this is our in-house compiler that can produce

um Halo 2 circuits and it's it's basically an improved system agnostic compiler right we have a current leader support for Halo 2 and planckish circuits so let me talk about a little bit uh the language itself um we decide to create this language in the same fashion as ml or Haskell so jubix is just another language in the ml family um and the main reason is because the Indians are just declarations about your

preference right so you specify exactly what you want but you don't specify how this really matches with the declarative uh style of programming and something that we decide like this is our design that uh design choices is the language is the static strongly type and uh the evaluation strategy is strict so we have strict semantics and we're just taking features from the mainstream languages so we have Purity we have totality so we need uh

uh we enforce your functions and your data type declarations to pass certain uh static analysis um you have immutability pattern matching trades referential transparency so on so forth so yeah so juviks is the is just dysfunctional language is uh is steering complete by certain annotations and you can go to the documentation we have uh provide a reference of the many constructs of the language and if you are more curious about uh the specifics of

the language we are also uh making some aspects some formal aspects about the language uh right okay it seems like I don't have internet here uh yeah okay yeah so we have in the language these characteristics which is referential transparency do you expect that a program with the same inputs produce the same outputs that's something that you expect we have some module systems so you can modularize your program you have top and local modules you can open in you have this open import statements so you can bring to the scope different

um identifiers names and you can select Imports you can hide things um we also have a red Ripple so you can interact with the language and we're very proud of this documentation tool is really nice you can just in the same way that you put comments on your code you can put Doc strings or kind of uh what you find in Haskell with hadock I'm gonna show you all these things quickly and we are just building an ecosystem around juviks so we have a few libraries already and I really expect at some

point people will start contributing to the to the to the ecosystem with your libraries we need cryptography we need uh many other things right so at the moment we just have support for data structures we have a property based testing a la quick check right and we have a unit test framework if you want to uh to do all right uh so Mayas how many of you are willing to try on your machine's Dux I hope yeah I will try it so uh the idea is just to go uh

like a very high level I will not go into the technical details um everything is in written form so you can just find it on the website oh really all right all right uh yeah probably uh okay let me um okay that's those are things that need to be double checked before right so uh this is our documentation uh the colors are not really

like you can see here um right so we have two options you can install on your machine we have support for Homebrew you can install the binary directly there are many ways that you can uh install javix and uh for this Workshop we also um have a code space so you just click here and this will open on your browser um juviks with all the environment in visual code but so right so this oh yeah I sold your your comment um so in the documentation we have uh installing two weeks and

basically you just can copy and paste this on your terminal execute this and you will uh install jubix otherwise you can now have mac Homebrew utility right okay um but I I really like this code space so let's just try this and by the way I included in the tutorials we have this CK submit right so let's try to follow this tutorial all together so the first thing is to install the ux

compiler if you want to just skip this process um just uh clone this uh this is the source of the worship right Okay so when you're creating the code space you just click here it will take a few minutes I think well okay well this loads let me see if I can say a little bit

right okay is there any questions so far about the language I haven't really show uh this learner's proof uh thing but I'm gonna do it the main intention for me today is that you get familiarized with this language and that you can leave the room knowing that there exceeds a new programming language that you can use to compile to Sarah notice proof it's a high level language and we are solving a lot of the problems that you uh face during circuit compilation there are very few and uh okay

so yeah this just build in okay so if you have on your machine visual code uh you can go directly and just put

here juvex this is our extension and then you just need to install it and something nice that we put here is that you don't need to really install the binary of jubix it will do it automatically and it will also install the binary for our in-house compiler the vampire one so you also have that problem solved once you install that my recommendation is to open a new folder where put where you're gonna put your files because extension needs a workplace inside uh for your files and

yeah so the first thing that you want to see is hello world right you want just to see how to encode hello world so every file defines a module and the module name is exactly the file name so you need to use the same name it's hello world in this case and this is a bit of the syntax I just want you to try this on your machines and just execute we include this through four buttons actually with this one you type check the code so you check that your terms actually correspond to the type you are annotating with right and you have also compiled because you can compile your

program to different backends by default is the native and you have also the play button so you can run this uh so in this case you will just see here hello War right and uh and for example as I said we have this documentation uh let me try to see it exercises that we include yeah so documentation just starts with three dashes and in visual code you just can press this button HTML preview it's on the top

and you get a nice looking documentation I'm gonna try um so you can use this to document your programs and this is a web version of the tiger simulator which is the example that I show about the intents at the beginning what is nice is that you just can click if you don't know anything in the code you just need to click on the identifier and that will take you to the definition right so for example here in the I know my intent uh API a resource is this record type so you have four Fields the first

one is a logic hash which is just uh not it's just an address that encodes uh where to find the predicate you can have for uh data types sorry other values and yeah so this is more or less how it looks and I'm gonna try to uh you to try this on your machine okay so this is visual code let's check it out if the visual code yeah so this is the code space just let me change the color team uh to something I don't know the light

is better or the dark light light okay perhaps this one okay actually let's just uh double check what we have in the readme I'll make disappear this uh oh uh I had okay yeah okay so we have worship exercises

good uh one second all right so in the code space um and if you follow the instructions a third doing the installation you can just execute from your terminal so here in your terminal you will you can have jubix it's just another this is the CLI and you have different options right so you can type check your code you can compile it eval and generate the HTML or something that we also include is uh this command

doctor checks if you have everything set up correctly you can initiate a project and there there are many other things that you can do for example if you're interested in compiling uh to serenology proof to circuits then you will go and write compile and then put compile help right and then you have our options right and you will be interested about the target so we have all these targets at the moment we have wasn't webassembly native we have Gavin vampire and current and Asm in the code space you also have access to the vampire

code sorry [Music] uh with this so vampire is the one is like our low level high level language for writing circuits so before you write a hello to you can just use a vampire and it will abstract many details that you don't need to know it has support for higher order functions uh and there are many things inside this compiler and then you can work with plug Halo 2 right but we want to do that in a moment

all right so this seems like we have everything set up all right um CK submit something as developers were used to also to interact so do you have this button over here is the one that loads the file in the rebel also you have this option and uh yeah and if you click on this this will open a terminal it loads the module and then you can ask things like you can add for example what is the

definition of booleans because I don't remember so then you get this nice output and also as I said if you don't know anything you just can click on a identifier just press command and we actually have two things so you can let's just close this terminal you can with your mouse hover the identifier and then you get this uh this information right for example it it tells you that uh this not type is just an inductive natural numbers

uh definition right and um and then just pressing command or just with the mouse you can go to the definition you can jump and see exactly what the things are right the definition itself yeah so with the compiler we ship also the standard Library so you don't need to care about installing a standard Library you just start importing it this way uh but yeah let's go step by step I'm just trying to show an overview of all the

features that you have if you use visual code we also have support for emacs in K2 or emacs user but the today I'm just using a visual code okay uh there are many things we're trying just to chip to make a programming language with all the advantages that you will find in a uh any other high level language right foreign so let me go for probably the most essential things right which is functions so in Python uh you will Define a function using the keyword Def

well in jubix you don't need it because you are just defining so many functions so we decide to just drop that keyword and the first part of a definition is the name of your function you can have arguments and then put a name for that argument and always put that type of notation so that goes after the column so in this case we're defining a function that takes us an argument a natural number with the name n and produce an output of type natural number what is a natural number you don't really need to know but if you want to know then you just uh in your code as I said command uh

click and then you just go and see the definition of it okay all right so if you write this well this is a function and it's incomplete because you haven't defined defined it the body of the function so you need to Define what the function does right and for that we have these assignment symbol so after this assignment symbol you define what exactly your function does and we have many uh language features to Define this in this case we just want to add one right so try to cut yourself on your machine this function it's just at one

and then you define M plus one let's try to do it all together so um I'm gonna open a file I'm just gonna name this um at put here jubix the extension will suggest to insert the module name I'm just going to click and after clicking I'm gonna Define the function so if I do add one and put for example Nat this is incomplete I just configurate a shortcut for the you can click here

on the check symbol to type check your code and then you get you get this error message right where whatever message is saying is that it's expecting the definition of the function so we need to use the assignment symbol oh and then I have Echo pilot so it can learn how to code javix already uh uh you just can put equals one and this is perhaps a name for this will be one right but it doesn't know what is not so we need to import the definition so we have a standard Library it's called standard

lip and then we have a Prelude with all these definitions and it tells you well done it type checks this is like the reward for you uh now let's define this function at one and the type signature can take different forms look this copilot is already too smart you can use it uh one thing about the visual code is that we have support for Unicode so if you press the backslash then you can uh have

really nice things like Alpha Beta you can put the really nice things but uh yeah so um uh what what I'm doing here oh yeah okay I'm just taking a number let's call it X or n doesn't really matter and then just x uh plus one right we have or you just can do it directly well done okay

this is how you define a language uh we have four constructs you can Define the maximum between two numbers the way that you do it is that just put the name for the two arguments put the type signature saying that the maximum of two natural numbers is just another natural number and you can use the if so you have a this comparison here and then you return what uh what is the maximum right we can just copy this from the from the documentation click here right so you don't have a you need to import this so we need to

import data nut or the open we need a relationship the relationship okay this type checks I'm going to try this right away I'm gonna use the Ripple and I'm gonna do maximum between 1 and 6. is six of course again if you want to know what is Maxima then you have the definition all right um I think

um something that we inherited from the ml family is the definition of function by pattern matching this is really convenient so a definition of a function by pattern matching is telling you uh well it's introducing equations for for the definition for example in this case we want to check I don't know if this is uh big enough we want to check if a function uh if a natural number is zero or not something that you will encounter in circuits well you can say the natural number can take two forms it can be zero and in that case you just

output true value or it can be the form of a successor of a natural number right and in that case you output false right this is the way that you split out the definition of a function and you just can take this and um type check if you want um well okay here it is telling me that um I don't have booleans so I need to include booleans but uh sorry uh it's actually about this uh

we are changing the syntax to make it simpler so right let's terminate this good and you also have support for recursion so if you want to check that a function uh sorry that the natural number is uh even per result you can you can formulate this function introducing these two equations zero is an even number so you uh just output true and if it's a successor you ask the same function to respond the question but for the previous number right

foreign you can type check we are again with the semicolon you can make this appear this and something really nice about programming languages especially functional programming languages that you can Define the a parametric type of list of elements of different type so we have support for polymorphic pre-next polymorphism so we have uh we can Define the type of list of a natural number the type of list of strings and list of lists so on and so forth but we already have done so you don't

really need to do this we are just uh declaring a lot of functions we have libraries that already provide solve this implementation details here we are uh here it show UPS uh the polymorphism so you have a variable a this is a type variable it's an implicit one so you don't need to provide it it will calculate the length of the list so the argument of the list uh sorry the argument of this function is a list it can take two forms it can be the empty list in which case uh the length is zero or it can be format by or consists of one piece of data of type A

and with another list right that's uh the Constructor of a list and then you have uh just using recursion the length of this list for example is just plus one right so you can use successor or plus one and then calculate the length of the um of the simplest in the case and we are really excited about this language feature is we can change the syntax uh there are many um things that we can do let me just reference where exactly you can find so we have some syntax extensions in the

documentation you can put aliases two things so if you want to name I don't know uh let's say that you don't want to use bull you want to name Boolean that type you just can put syntaxes aliases here you don't like fault you want to be very logician so you use use the Unicode term you can do these things whatever things we have iterators so it's not really usual to find these extensions I I actually I haven't seen this uh in other programming languages I

like to do rigs but we have these iterator syntax we can tell I'm gonna Define an iterator like a four Loop that go from a starting point here and goes to other uh bound right another syntax extension that we have with fixity so you can Define different fixities um this is more like if you are defined your own operations and you want uh to be a binary you want to define a binary function that is associated to the left or to the right or that it's equal to

some other operator uh and then you have uh lattice basically to resolve the syntax so that's another facility that we're including and we are also having this uh operator syntax to um in this case this is this is very uh this is very nice in my opinion you are defining the type uh the product type which is just taking two piece of data of different types the Constructor is just the parent right the type for the Constructor is just a function that takes something of the type A something of the type B and then

you construct a term of the of the product type well here you're using this time symbol this is really nice but you can say okay this time symbol is just another operator for the product and the product is just a binary uh uh binary operation and then you are free to go you can use the time symbol everywhere and this uh will resolve again if you don't know anything or you just miss uh something that I said you just use the search bar you can go for operator here and then this will take you exactly to the place

we're trying to document all the things you can do with ux all right uh let me see what else do you uh do we have butter matching polymorphism iterators uh uh yeah right and then we have the exercises okay so how would you define a function that takes a list and zoom up all the elements in this list well it's a function let's call it sum

the argument let's call it excess and then you have the type of this is the list of natural numbers and because you are swimming up you are getting a value of the type uh nut this is the type of natural numbers and then you need to Define some way to do it so the way that uh you can do it is using this iterator syntax we have these four so you said okay I'm gonna Define a four similar to python a little bit you have an accumulator this is a variable where you can put values in it and then you can iterate in the list this is the syntax you say X in the list excess

and then in the accumulator you can put this value which is the element that you are current visiting plus what you had before accumulated right this is really nice nice because you then can simplify a lot of the common function that you will find in functional programming languages you would uh usually use fault left right and that well it's really nice but we already have these convenient functions uh yeah

the list of any objects lines throughout some discriminated Union of what it is at one time and then apply the code yeah it's a statically typing fully stuff when we talked about the compile time yeah okay yes yeah and uh something that we are trying to enforce at least but for now is that is uh typing is as I said is required so it's like a discipline um maybe it can be seen as a drawback but in the long term it's a good investment for you and for the sake of your users um

yeah we have a type inference so uh the core language is actually uh anti-blum the calculus with an option at typing and we have um underscore so I can so in some places you can put for example let me see this works for example here right so you can infer what is the type of one right this is fine when so we have an algorithm that we have type inference right but you cannot skip the typing and by that is what I'm

trying to say is that you cannot skip the colon type but we have this underscore which is the device that you can use as a placeholder you can ask here for example where is the type of um what is the type of one so let's do it so you can open the Ripple here um and then I think it was colon T but let me double check I know is yeah column type okay so you like uh type and then one and then you get not and if you are

[Music] discipline so you put here not so you can interact with the with the Red Bull and try to make uh your program well specify I think it's a good discipline also I'm a fan of of type so the maximum expired place I'd like to apply that to anything that supports right so this in particular you can see that I'm just getting the definition and you you have the two arguments not so in that case I can infer that as well

yeah um there are other places where it gets more uh challenging so it spits up you know 40 gigabytes of uh uh specific for the underlying types of crime Fields yeah um yeah there is a step going to vampire that we need to uh more and more size

the uh the code and so we will be very explicit about all the types inside the inside of the type signature so yeah there is no so much room to screw it up here if yeah right um on things that you will find and um I'm really sure that this will become really uh mainstream yeah and the future is uh mapping and filters like this uh functional program Paradigm of these facilities that we are shipping in ux and you can find in Haskell or or camel or and lean this will show up in all other

programming languages you have mapping you just sent out uh this is just an abbreviation for for a function that just takes a list and then you evaluate the function in every single part of the list or you can filter out things so yeah this is this is the syntax I think it's it's a really nice thing for you to try so we have these exercises uh we have 10 minutes so we can probably pick one um

let's try to do the exponentiation right or the you know you also have maybe uh things so you're not missing anything here everything is going to be online so if you cannot follow the tutorial today just sit down next day or whenever uh is better for you and just follow the tutorial so if we try to do the exponentiation um exercise and you download this we have this file maybe you didn't notice but we have a statement to introduce things without definition

and we call that axioms so if you don't know uh the definition of a term and you want to use it you can put action that basically tells the compiler that that term doesn't have any uh computational content at the moment right and if you later find out what is the definition you just can remove the keyword action so if you have exponentiation here let's just try to Define this right so how would you define exponentiation let's say that the first argument is the base and the second one is the um the exponent right

I would like to be the secretary here so if someone tells me okay so this is exponentiation takes two arguments X and n and we're gonna do it in the same fashion of pattern matching so you need to pattern much on nuts so so you have X and then you have zero what is the result oh we have the co-pilot that

says as one right all right if you oh man you can't use the copilot and just write the definition for um right uh you don't need okay the pilot scrub here so if you have eggs and you're trying to uh have n plus one then you just need to multiply the recursive call of X with n then you're free to go it's not soaked with the the whole series with one C

um what is going on here uh let me all uh we probably gonna change oh sorry uh right well actually yeah there is no need for putting this X uh what is going on uh the column yeah semicolon

no there is something wrong uh well that's why you prepare the solution in case you cannot handle it oh yeah uh so one one thing is that when you introduce names before the colon in a definition you introduce that variable here is not uh necessary so um yeah actually yeah we're just gonna copy and paste this but it's essentially you just need the X to have a name here and then the exponent you can just butter much and get uh one good

um but before to let you go let me go to the to the main page here we have by the way we have blocks and we are describing some parts of the internals how to compile vampire through Gap this is important if you don't want to go for the direct approach of compiling to circuits this is a evaluation interpreter approach to compiling functional programs to circuits and the other approach that we have is juvex to vampire directly and in this case we basically just take

the program and remove all the features that vampire doesn't support to compile to circuits and we have a blog post about that and it also takes you to all the examples all the instructions in the main page we have this a small example so I said to take the juice file you compile to vampire then you can go to Planck or Halo 2 so you just need to specify the target your file this is your file for example here we're just defined in a hash function is the mid Square hash function in this part we have

the definition of exponentiation by fast uh is the fast algorithm where you basically put the exponent in binary form and then perform stat you can say that the program is terminating and we have also pregnant for unrolling uh recursive functions which is some of the challenges that we have when when compiled into circuits this is probably going to change for the moment you need to explicit you need to be explicit about how many times you want to enroll your functions otherwise you cannot compile the circuits right we're investigating how to remove

this uh we we have some ideas and the main function that you're gonna compile to has two um sorry it has one input in this case it's not and will produce a nut and this is the instruction that you need to perform so you take the vampire you do the trusted setup with the parameter right and then you specify that you're gonna use Planck compile using the inputs uh this is the output that we are heading so in the code space or well if you don't have the code space

I think I need the code space okay in the good space you just can copy and paste this on your machine and uh you will get also taking the inputs you will get the results let me see if this is already loaded okay so there are many things that that are missing and uh or things you can generate the proof uh with these commands and verify as well that's part of the vampire uh topic okay

uh just uh before just one second everything about joox is open source so you can just go um go and see all the the compilation parts this is a really basic example of audio mix it's just comparing that the natural number is zero and uh yeah you can compile this to to vampire if you want to know more specifics I just can sit down with you and show you uh exactly what to do if I don't know the answer I can point

you to the person that knows how to solve that thing but I'm very confident that I can answer any technical question with more time I don't have just I think just have one hour all right I'm very excited if you have any feedback I'm really interested if you want to use jubix or any of of the intermediate languages we are doing integration with cklbm that's in our project and yeah we can basically just talk to you about the internals and probably get uh uh more integration with the CK

ecosystem so it's not limited to anoma but is mostly focusing on providing the next language for anoma the apps that's where I wanted to transmit communicate today all right yeah you're correct so it's like an immortal uh especially man yeah so we hope juviks don't die foreign the language right

right so that's part of our um roadmap like in the moment you need to use these uh let's call it primitive API for uh tiger and uh but what is really important is that we are the design designers of the language the developers of the compiler so we can change anything in the in the language and of course we want to make this much easier to follow uh that's why we are including this syntax extensions and many other facilities for you to basically not write code they call synthesize bunch of code and

get some people they look like really basic stuff yeah we're gonna get some applications and um um what I foresee in it is that once we start doing those applications we're gonna change uh more the language so so far we are just putting the ground for for this technology but it's

oh yeah but that's uh an issue that it's not concerned to to the language it's more on the on the component that resolve the intents right so uh that which is actually quite hard problem computationally speaking yeah you want to retract to retract from the I don't know all right uh yeah I'm not really familiar with that scope of the application maybe you can answer or I don't know

yeah but yeah it's probably very concerning any more questions what is good actually yeah so uh that's actually a quite an interesting question to solve so um just for seeing these we include so we have a report about what is gap but it's essentially at the moment like a language for doing aromatic circuits via category called semantics so to speak so it's our alternative to not tell the

compilation uh as usually we will find with other programming languages that Target circuits so we basically observe that you can just see a language as a category and then you have functors so at some point we want to evaluate the program that represents the the circuit and then in that sense in that context we want to avoid problems like the branching problem right so it's our detour in order to solve one of the issues that you basically will face when compiling to circuits so yeah Gap is this

is I would describe it as an aromatic language for the moment using the um categorical terminology right like it's a category like finset basically yeah but I can point to you exactly what is the definition which is not uh yeah the specifics yeah [Music] so from the juvex point of view we just

compile natural numbers to natural numbers to vampire but the in-house compiler which is the one that takes uh the job I'm not entirely sure what it's doing but yeah so the the piano this definition that I show about natural Lumber is compiled to natural numbers sorry natural native yeah that other efficient yeah you don't exactly you don't want to to describe natural it's just that this definition for natural numbers is

convenient when you are defining a function uh by pattern matching but uh you don't want to compile this like uh this way but no we we have this annotation built in that which tells the compiler that these uh type definition corresponds to natural numbers so we have a special compilation phase four for this uh yeah yeah how big is it um I tried it range up to 2 power 62.

yeah it's not um yeah it's not 64 bytes it's just 62 but we are planning in our roadmap to support big integers which is challenging as well yeah any other question no okay [Applause]