#239 Grigore Rosu: The K framework - a framework to formally define all programming languages

Transcript

[Music] this episode of epicenter is brought to you by shape-shift I owe the easiest fastest and most secure way to swap your digital assets don't run a risk of leaving your funds on centralized exchange visit shapeshifter i/o to get started hi welcome to epicenter in cryptocurrency podcasts that covers upcoming technologies companies and networks in the blockchain and cryptocurrency space

I'm ahead Roy and my name is Sonny Agarwal and today we have with us Gregori Rosso a professor of computer science at the University of Illinois urbana-champaign at the CEO of run time verification nice top you on on the podcast Corey can you tell us a little bit about yourself thank you having me oh hi so yeah my name is Roberto Rosa and I I came to that estate in 96 to do a PhD at University of California and then I was always attracted by mathematical techniques and foreign methods and I had the privilege to work at NASA for two years before joining University of Illinois as a computer science professor

in 2002 and since then I've been there all the time and I started a company run time verification in order to take ideas that that we initiated at NASA Ames actually that's what we coined the term run time verification at NASA Ames with colleagues there and and the plan with the company was to take all these ideas and technologies developed mostly by researchers and academics into real-world products that that can make a difference so that's how we started a company awesome and so that and the sort of the end result of that was the K framework which is what we are discussing here today could you tell us a little bit

about what originally got you interested in programming languages and formal systems so I started off as a mathematician and and when I joined NASA my job was to to prove that programs were correct that that certain flight software was safe and I started asking myself what does it even mean what does it mean for a program to be to be correct um so so let that what what to started me to think about about formal methods about how to how to mathematically capture the meaning of programs and and then I was fascinated by by by programming

languages by all the variety of programming languages and paradigms and in the end realizing that every single one of them had a very deep mathematical meaning and once you capture that meaning then you have the language in your hands you can do everything you want with it you can execute programs you can prove programs correct you can do everything so I found it just fascinating and once I once I once I once I realize it I was I was trapped into this field and I just loved it I say cool and so I also read that you know K actually originally started off almost as a teaching tool as a way to like teach students and then it ended up a ball thing out of that could you tell us like you know it doesn't still have

that goal of being a teaching tool or has it grown much beyond that original vision well first of all I still use it for teaching I used it last semester no teach it I remember someone takes next semester also using K so yes you've started from teaching means when I joined the Department of Computer Science I was asked to teach programming languages actually I was asked to teach programming languages even during interview I really need somebody to teach programming languages and and since I already had some ideas how to how to do that formally from NASA I was very glad to pursue this this path in my in my career namely to teach programming languages and at the same time to

develop frameworks for it and I found actually is that so obviously initially I didn't think about ki had to teach programming languages so so and I knew that it had to be somehow mathematically gross and and I looked at a variety of approaches that were available and I tried every single one of them I think I tried eight or nine different approaches like operational semantics most a big step denotational semantics evolution context reduction semantics with continuations and and in the end we came the chemical abstract machine was really interesting and and any general I realize if each of these had a very nice idea under the hood but at the same time some things were

missing from each of the approaches which kind of motivated the other approaches that are invented right so people invented different approaches because the previous approaches were missing something and what I really tried to do with K initially was to just engineer engineer a framework which takes the best from all the approaches that that that we had around and try at the same time to avoid their limitations I didn't think at all of the mathematics underlying it I knew that once it works from a practical point of view we'll be able to come up with the mathematics because all these other frameworks were based on rigorous mathematics so the challenge was really how to make it easy fun and modular to define programming

languages because one of the big problems when you formalize a language is that you add a new feature to your language and then you have to go back and change everything you've done in order to accommodate changes in the configuration the program configuration needed for the for the for the new feature and that's very inconvenient a very tempting motivating imagine that you have already put hundred rules and you add one more feature and you have to go back and change all the 200 rules that will feel very de motivated to add new features and and I was lucky enough that I was now in the middle of a very nice group of students who were very enthusiastic to use the early prototype to define languages and they used the

language and I encouraged them to complain so whenever they had issues I wanted them to complain and they came I said look I don't like to duplicate code I don't like to duplicate rules I have to write the same rule again and again and again and that's annoying all right thank you thank you and then we try to engineer it in such a way so that doesn't happen right so so that so that you define the language in a nice incremental constructive way without having to go back and change either to very defined in order to accommodate new features so yeah so we engineer the framework and then the mathematics game they put everything together in a nice round thing so so of course like this episode is about the key framework and as I understand it professor the key

framework is an attempt to have mathematical structures and rules and ways of expressing rules that allow people to right the rules of any programming language it is essentially a language with which you can write the rules of any programming language is that right it's almost like a one ring to rule them all right so we as programmers we use a language to write a program and like there's like hundreds of languages around the world and the K the K framework gives us tools and semantics to express all of these languages in one unified mechanism yes

that was the the goal and and that's what it is and you can think of it either as a meta programming language in which you define programming languages or another way to think about it is like a domain-specific language for programming languages and in fact you can even define K in K which is what we're doing right now so are the implementing when implementing K into a right because K is a language in the end and it needs to be expressed in itself and many programming language is actually implementing themselves you know even Scala and in other languages so right yes so so the challenge the challenge was how to come up indeed with something very uniform that allows you

to define any programming language in any paradigm using the same general principles and what are the general principles so that is possible and in my classes where I teach programming languages using K we actually go through various programming paradigms we start with imperative languages and we move to functional languages then we go to object oriented languages and logic programming languages in the end in students have all the kind of projects along the way where they combine features so yeah and in the end in the end it all boils down to a very simple principle which is that of a parametric transition right so you have a program

configuration which you can think of some data structure that holds a snapshot of your program state and the same happens in all programming languages no matter what paradigm you use you have this program configuration and then you have rules that match certain structure they care about in the program configuration in particular the fragment of program the students to execute it for example they match whatever part of the configuration they care and they apply transformation so match and apply so basically the red rules are pattern relates to butter so you match the left head button and you replace it with the right hand pattern modulo the substitution of the variables that that

results from the from the matching process so that's it there's the only computational mechanism under the hood and this is to incomplete it has been shown during complete many many years ago by many people in different settings so it's a very powerful computational mechanism and what makes it interesting philosophically speaking at least from my point of view is that it allows you to tune the computational granularity of the computer of the computation the granularity of the computation for example when I define a Turing machine or lambda calculus the generality of the computation is given by the construct that you use so with general purpose writing term writing like K employees

you can define that granularity by means of structure to define your syntax and then and then rules match as much of the syntax on to transform in one step you do not have to reduce it to lots of smaller steps to perform a big computation can judge it do it with a big matching and transformation so yes yeah so that was the big challenge and as I spent quite a bit of time back in 2003 2004 when the whole thing started thinking about what would be the right mathematical formalism to employ in such a meta language framework and I looked

at existing approaches and writing term writing really was the most appealing to me exactly because of this capability to match as much structure as I want from the program configuration and then the figure to are able to define languages in across different paradigms quite easily and naturally that was like a bonus like a like an additional incentive to convince me that is the right way to go interesting so of course like so later on in the show we will get into some of the some of these details that you're pointing out is the idea of the rewriting logic and and and how that works but zooming out for a little bit

this seems like a a language in which you can express any computer language like this seems like a very very interesting idea when when when you tell it to anyone do you like how old is that idea and why did people think of this idea in the first place we're so yeah yeah is very very old lambda calculus itself is based on the same idea lambda calculus actually has only one rule which is beta reduction you take a lambda abstraction applied to a turn and the transforms into something else but it is just one particular writing over one particular symptoms in k we want to have any write rules about

any syntax and in particular like and you find out that calculus editor is a particular theory in our particular language in in K the same way you can define other other formalism other imperative language is based on assignments based on so the sort of writing is an idea when he started I don't know but it's definitely a very old idea I think maybe grammars in the theory of of context-free grammars we had the first the first ideas around writing maybe even even before even before in early night nineteen hundreds right even before we had lambda calculus and so many problems are not expressed

specifically as terminal writing but they were instances of the idea of done writing the term rating idea so yes it is very old I would say what is new perhaps is the particular methodology on how to use writing and how to organize your configuration and what is really important is how to find the place in the configuration where you want to apply a rule because whose not always applied at the top level in your configuration that you have to find the right place where to apply the rules and this is where you may need to specify context context are actually critical for for efficient implementations and effective implementations of writing so

yeah I would say the writing itself is not a new idea and even context they are not very new and the framework itself was engineered from many ideas that were floating already in the programming language semantics field but I think what Kay really did well of course I'm biased but I believe that what he did well was to put all these ideas together in a in a in a meaningful and practically useful way without without worrying about the theory initially and then when we came up with the theory I was very pleased to

see these things fit so nicely mathematically as well so we developed a logic a foundational logic underlying the entire key framework which now explains everything we do so everything we do in the key framework can be explained as a search for a proof for a fact right so everything we do in the end is very rigorously backed by a mathematical proof starting with execution verification model checking symbolic execution everything is backed by a proof I think that's where some of the innovations on the mathematical side the key thing what happened so I could do look maybe for some of our listeners

who are less familiar with like programming languages you know could you explain to us a little bit about what the difference between like this syntax and semantics are and how you can use rewrite rules to you know it syntax is usually about like explaining what the vocabulary is well semantics is more about what the grammar is and it seems very easy to understand how you would use like rewrite rules to explain syntax but how would you use these to explain semantics I can you like talk a little bit about this in fact in fact I teach parabola which is to to fresh students and I teach prime limited using K and syntax and semantics is defined in K and they grasp

it right away even if they do not have a lot of experience or even if they only know one or two parameters they grasp the idea because it is so simple so in terms of syntax yes of the different in syntax and semantics so syntax is about really taking a string write a program what is a program I probably just a string of characters right you can think of it that way some you know level of abstraction and then you have to give that a meaning but before you are ever able to give that a meaning we have to realize that there are some constructs there right there is an if-then-else construct there is a wild constructor is a function defined right so how do you go from flat sequence of characters to a tree and abstract syntax what we call

Kafka syntax tree basically a term that corresponds to the program how do you get from the syntax from from the strings to the program but that's what the parsing does and rot so passing is not new parsing is a very old field there are lots of algorithms some of them more efficient others more general and and in K we employ both efficient and general algorithms you can define a sugar and parcel outside of the key frame or the key from my perspective is your general powerful algorithm which is not very efficient but very general and and yeah so basically the syntax allows it and K has this key word syntax that will define syntactic productions for example reason it's an expression is an

expression the simple plus another expression write an expression can so be an integer for example right and now if a1 plus to the parser that you generate automatically from this the syntactic definitions the parser will will will give you a tree a nice after syntax tree where you have 1 plus at the top and then 2 to the right so now you finally or you have some structure right so once you have some structure from from your original program now you can talk about semantics so what is the semantics the semantics takes this structure these three is this abstract syntactic trees and gives them a meaning and now depending on which much work or formalism we employ this

meaning can be expressed in one way or another but in all approaches in the end what you get is some sort of mathematical object that corresponds to that syntax that you started with and in our case in the case of K the way we add this meaning to syntax is by means of rewrite rules where we transform iteratively this tree into a value R as deposit or program was 1 plus 2 right so the parser will give you 1 plus 2 nice tree with plus 2 the top and one into the left and the right and then there is a rewrite rule saying that if you have an integer plus another integer is rewrites to the sum of the two integers in the in the mathematical domain right

so with one rule you transform that tree that has three nodes 1 + + + + - you transform it into just one node 3 which has the value 3 alright so so the semantics is obtained by iterative transformations of the original program you start with the original program you put it in some some configuration which contains alteration information in order to run the program which could be like like a state stacks and all kind of addition infrastructure that you need in order for the program to make sense and then step by step applying rules one by one transform that into a final configuration which contains the result

of the program that you're looking for so I'd like to restate restate this in in my own way right so we can think of let's say we can think of human languages first right so in any language so for our listeners any of you that has learned a new language you would have learnt like vocabulary and then you would have learned grammar so vocab but what is vocabulary vocabulary is like oh I let's say I'm about to learn German and vocabulary is like so there is a spoon and then

there's a word in German so let's say like there's a wolf there's a fork and there's gobble so gobble means fork in German so it's like vocabulary is the association of a word which is like gobble to this thing which is like a fork but then there is also grammar which is like once you have a lot of words how can these words be arranged together right so in some senses what I feel professor is like that semantics is the computer science equivalent of vocabulary and syntax is the computer science equivalent of grammar right so for example like if if I want to tell

the computer that it has to it has to compare two things and if they are equal do something so this is like an operation and semantics is like what word does the programmer use to represent this operation and syntax is what the way in which these operations can connect together in order to make a well-formed program this is that right it's almost there is a bit more going on in a computer program right because in natural language you just say something is a sentence and and your sentence doesn't have to compute into a result reactor sentence is being

parsed using the grammatical rules and then based on the individual meanings of the individual words right in the vocabulary you then build a meaning for the entire for the entire sentence right without having to execute right the the sentence so in some sense if you think about what K what we do we take such a sentence which would be the program and and then we transform it step by step into another sentence which is a bit closer to the final result and then into another sentence into other senses until Indian becomes three you know the final the final result right for example here is a sentence let X be three in the expression 1 plus X all

right so what is the meaning of this sentence right you may think it is 4 right because you say let X equal x be 1 in 1 plus X but it is not immediately obvious unless you do some computation there so you can parse it and you realize okay I have the key word left which is like a statement then I say oh the variable X which is equal to 1 so I can use all the grammatical rules and I can parse this sentence into something that now I can add semantics to and how we add semantics to in this particular language would be that I just replace X I transformed the senses that x equals 1 in no let x equals 3 in 1 plus X I

transform it into 1 plus 3 how I just realized that I have a let construct and let x equals 1 in some expression means that I should go ahead and substitute one for X in that sentence for three for X in that sentence and the remaining of the center's which is one plus X now becomes one plus three and then I apply another rule which states oh one plus three this goes to four right so I go in one more step so it's like if I keep talking keeping talking that's what you have on original sentence which you parse and then gives you the program but then you can keep talking about how that

program computes right and then you come up with the result in the end and I would say that the syntax of K is the part which allows you to parse that sentence so you can start transforming it and then the rules are the keep talking part right which allows you to eventually get the result for the whole program okay for example if you have a Java program you have a for loop or a while loop right so that computer may execute it like like a thousand times you may do a very complicated computation there how do you know what the result but you have to simply go through the loop step by step by step I said like working through the program and and that's what the rules of K allows you allow you to do so sometimes

I I know that the word rule may be confusing because you have rules for the grammar and rules for the computation the roots for the gram are allow you to parse and the rules for the computation allow you to compute ok so I kind of understand this now umm what is the what are the benefits of like formally ah like of these formal semantics cuz like we have like you know hundreds of like common programming language is already out there and most of them usually aren't formally specified they're usually like you know oftentimes sometimes they have reference implementations or sometimes they have like guide books but they don't really have like they don't they're oftentimes

you find like undefined behavior and whatnot what are some of the benefits of having this like formal specification of every language that's actually a very good question which students often ask when they take the the class program um again we start talking about formal semantics so here's my short answer so what is Java a fast what is Java whatever Oracle country it is well but if I want to if I want to maybe Java is it's clearer by let's let's consider C because you mentioned and if I behavior ok C is full of undefined behavior so what is see right

there is an 800-page standard which is an iso standard like a hundred pages of text describing what c is more than half of those pages is about defining undefined behavior right what does it mean for the C program not to be a correct program right some of something's obviously division by zero yes or access at i/o you know out of bounds of an array raven array right the numbers from 1 to elements from 1 2 or 0 to 99 and now you access element 101 is that correct or not so she will not check that for you you can access it and get some number or crash or whatever so so here is the question out so what is C and and why do you care about what you see suppose that you have a pacemaker right the page Michael run the C program

ok how do you know that let C program does what it's supposed to do because otherwise you'd die right so what if that C program does an array out of bounds access or a division by 0 and then you have a problem right to die so what would like ideally is to have a way to say that that program does something and this is where formal semantics comes to the picture without a formal semantics you do not know what the language is with the definition in mathematics right to only hit the finishes were to prove facts in order to define concepts right otherwise we cannot reason about those concepts so if not to reason about programs you want to say anything about the program except

you know waving hands but you want to say anything about a program you need a rigorous way to say what a programming language is or what the program is and this is where the formal semantics comes to the picture it's basically that link that is needed in order to do reasoning about programs this episode is brought to you by shape-shift the world's leading trustless little-ass exchange quickly swap between dozens of leading cryptocurrencies including Bitcoin ethers e cash gnosis manera golem or cur and so many more when you go to shape-shift dot IO you simply select your currency pair give me receiving adders sent the coins

and boom shape-shift is not your traditional cryptocurrency change you don't need to create an account you don't need to give them your personal information and they don't hold your coins so you are never at risk from a hacker or other malicious actor shape-shift has competitive rates and is even integrated in some of your favorite wallet apps like Jack's so you can swap your digital assets directly within your wallet just as easily as putting on your slippers whenever you see that good-looking Fox you know that's where shape-shift is so to get started visit shape-shift I owe and start trading and we'd like to thank shape-shift for their support of epicenter so one of the reasons that like you know for example and see oftentimes things are left undefined is

because like it allows for the some freedom to for the compiler to do optimizations and then you know oftentimes you can use likes things like linters and stuff that's the warnings that use saying like hey by the way what you're doing is unsafe but you know will let it happen because the compiler might want needed for some reason so what are some of the trade-offs that you do thereby like you know restricting the freedom of the compilers so yes yes that's why she has the undefined behavior because they want to allow compilers the freedom to do whatever they want basically more or less with undefined programs and to optimize so see one of the main

applications of C is is in embedded systems where performance is critical and and to achieve performance we to take advantage of the hardware to the last drop of speed and compiler developers didn't love that how to translate programs into something that is really very efficient on the target hardware so so for example let's take let's take actually array out-of-bounds access right so if you want to be absolutely safe you would have to check that you do not access the array out of bounds but then you have to pay the price the cost of that checking right you have to read the value evaluate the

argument and see that it is between bounds right so that costs more that it costs to actually access the array and that's unacceptable for for these people so what is should be see is that the programmer knows what she's doing and and and because of that we can assume that the program is well defined and then compilers take advantage of that and try to make the program as fast as possible that is great is part of the spirit of C the so-called spirit of city of movement in C however if your C program now runs in a car or in a medical device that your life depends upon or in some spacecraft or aircraft then you cannot afford to have unexpected behaviors of the program

and those unexpected behaviors happen all the time you see when we change the hardware you have a C program they look seasonable to you you run it on a particular desktop you test it looks great but then you put it on a different device money from plasma and it gives you a completely different result and you may die literally because of that right if you so you cannot afford that if you cannot afford that and many many embedded system applications where correctness became paramount in C programs and that's where the formal semantics comes into the picture the now what I can do I can take that program and I can analyze it to the formal semantics of C which defines completely all the undefined behavior in the standard and now that tool this formal semantics framework a framework

actually you run with the C semantics its input will tell you whether your program is undefined or not and if it is undefined you'll know you can still ignore it if you want to you can still compile it with your favorite compiler knowing that it has some errors but at least the framework tells you that hey you have an undefined program here be careful if you are not careful it's it's your inter it's your risk you are taking in there are some tools like the link tools that you mentioned which check for some very simple link style so call in style errors but far from all the undefined behaviors some modify behaviors are very tricky you know in C so so basically what will happen is like

you know I have a C program and I'm doing some sort of weird undefined behavior let's say doing two right on the same line or something right what what what uh what K would do is basically like throw me an error saying hey by the way this behavior undefined it doesn't actually make like a choice on what to do it actually instead of like you know a compiler would usually do that pick whatever it wants to do you instead will throw an error saying this is not allowed at all yes yes okay definitely yes and and then if you you can go further and actually prove the program correct you can program does what it's supposed to do in which case you go through all possible behaviors no

matter what input to the program is and you showed exhaustively by what we call exhaustive runtime verification go symbolically on all the paths that can happen in your program and you prove that there is no undefined behavior no matter how this program executes and this this particular feature became extremely useful to companies like NASA Boeing we have several contracts with this we use the Kree framework witness II semantics for exactly this purpose so could you expand a little bit understand like what is exactly is the relationship between like formal verification for no semantics because oftentimes like people think that formal verification is like strictly in the realm of functional programming languages people like oh if you want to form on vacation you need to

use Haskell or Oh camel but now if you're saying that we have this Wade K provides us like a way we can do formal verification of C programming and stuff do you expand a little bit more about this so I love functional programming myself right and I often founded a function programming community is a bit too enthusiastic about functional programming in terms of verification in the sense that they try to encourage people to storm ability to use functional languages because the promise being that it's easier to verify your programs I think it is easier to understand the program's the functional programs it is easier to reason about

them in your mind but in terms of actual formal verification things are also difficult to verify with functional programming them especially because when you functional programming languages are not as pure as the original lambda calculus was once you have side effects once you have a heap once you have references things can can be quite quite hairy what we did in K actually was to step back a bit and look at what is the actual foundation underlying all programming languages not only functional programming languages but and this is rewriting the term rewriting capability functional language is also do writing imperative language is also do writing

and and object when T language is also writing and in a logic programming language is rewriting so there is this basic foundation that goes beyond all the particular paradigm including functional languages and yes also I wouldn't say that it is necessarily easier to verify your functional programming languages I would say that a lot of the functional of the of the program verification work so far was by means of what we call for logic or axiomatic semantics where you have to

essentially redefine your programming language as all logic I know this may sound a bit heavy if you don't come from the field but you literally define a whole logic corresponding to Java that will have proof rules you have theorems that you prove and all these effects about about programs and and the rules for Raj X or axiomatic semantics tend to be a lot more involved for for object oriented languages or for or for imperative languages then for functional languages so if you follow the traditional formal verification approach then yes it may be easier to define an

axiomatic semantics then for a functional language turn for an imperative language that you can then use for formal verification but what we deliberately decided in K was to not have to define another logic for a programming language in order to verify programs so we want to have only one formal semantics of the programming language and to derive program verifiers from that semantics automatically essentially it is in some sense like like defining a whole logic automatically or deriving the whole logic automatically for your for your language from the formal semantics of the other programming language this is

not a traditional approach to program verification this is very important to to clarify and I am ready to ask this question because I think this is one of the critical insights of of K as we take an operational semantics and inheritor executable semantics that gives you a reference model of your programming language that you can use to run programs run tests same like compilers for interpreters but at the same time it gives you for the exact for the same formal semantics it gives you a program verify that you can use to verify programs and that is silent and what we call relatively complete so its sound and complete so any property about any programming language can be proved with with this length dependent framework and logic underlying

it that was one of the biggest theoretical achievements behind behind the keyframe or this foundation which shall also to detach yourself from having to define you know a whole an axiomatic semantics for your programming language only for verification primary education reasons you get a formal VeriFone the formal program verifier for your language exactly the same way you get execution engine or the parser completely automatically from the formula semantics of the programming language okay so you know the tagline of K is that it's this rewrite base executable semantic framework so we've talked about the rewrite base we've talked about

semantics and framework let's talk about this executable part what does it mean for this framework to be executable and how is that and like our other frameworks in the past been executable what does this exactly mean but I say the cutable means that you can take a program throw it to the framework so you have the framework and take a programming language semantics first right and instantiate the framework with the semantics and now you pass a program and the framework will execute the program the same way an implementation of your language would do right if they can see let's say you take a C program right and you compile it with GCC and run it right so actually our tool that incorporates the system

and is in the K framework is this frame is a replacement of GCC as a drop-in replacement of GCC which we call KCC right so so with our framework you just say KCC your program dot C and gives you a binary and you run it just what I mean by executable it is as executable as an implementation of a programming language and and that's funny because that's how I indicate my students right there for the formal semantics is and then they they have this face but why why would it be any other way isn't that what the formal semantics should be you should be able to execute the program and then I have to refer them to axiomatic semantics or for logic where I define these logics for people's

conditions and in volumes and so on where you can prove programs correct but cannot execute them if I have a loop that executes to how many iterations I cannot just run the loop with the whole logic I can prove the loop correct if somebody is giving me an invariant but I cannot run it and and that's very inconvenient because imagine a special key for formal you know logic for formal semantics using axiomatic semantics or ecology for a programming language it cannot execute how do you know it if it is correct or not in the case of C the systematic says I think almost 5000 semantic rules now 5000 rules in the semantics okay that people had to sit down and run and test test is a key word how do you test them how do you know

that those are right because like anything be a same lattice can be run when you add thousands of rules something may go wrong somewhere right how do you test it it is it is extremely funny what they should be able to take programs that compiler developers or or interpreter developers used to test their implementations and to use exactly the same programs to test their semantics and then to use exactly the semaphore program verification but as opposed to catching errors only by proving run programs correct or not being able to prove some programs that look correct correct right which is how you catch errors you know in conventional program verifiers so how does the how do

you verify the binary like the whatever or K is running okay sir is it compiled or interpreted but like how do you this is do we write like the x86 architecture assembly in K and that's how K knows how to compile to that or like what how do we verify the actual execution of the a language very good question so there are different ways to do it so as a matter of fact we do have a 70s of x86 that is in the process of finalising which means that you can then use GCC compiler program to x86 and then

run the x86 with the K framework but that's not what we do with the KCC tool the alternative especially have a formal semantics of C itself without any translation 20 singles and then you run the C programs directly with add semantics as the tonality the granularity in 10 eternity of the C language without any translation to another language because typically want to translate from one language to another you lose something in the translation or otherwise you have to prove that you lose nothing and that's extremely difficult as a matter of fact we we found several program verified for see that lose undefined behaviors in the translation because they translate from

see some intermediate language that their preferred knows and as part of the translation they they lose behaviors for example they may reorder the arguments of a function or they may order the arguments of an operation of primitive operation you know as they translate and all those may may eliminate undefined behaviors so yes wiki doesn't have an actual binary at all okay doesn't have an intermediate language at all so K works directly with the syntax of your programming language that's why we define the syntax and general semantics and your syntax give you the actual structure on which you want to define your computation granularity and then the rules F that competition grammar you to your desired

syntax now if you want to implement a translator from that to another language you can either implemented in K as well also using rules as a matter of fact we have done that for for a language called pluto's developed by IO H K and we implement a translator from that language together where ala is a low-level language that that runs in a virtual machine from you talk about who that shortly so so yeah so the translator itself is if I'm editing K rights okay can implement translators but also direct semantics of languages and the Ken K does not have like it sound binary language it's not like x86 or LLVM it's not like that it is not something to

translate your language into it's something in which you define your language exactly the way your language is without any translation so the future essentially with with Kay is you define like let's say we are talking about any language like JavaScript so the semantics of JavaScript are expressed in K and of course like once you express the semantics of JavaScript or in K you will get all of the tool sets that are required to actually execute JavaScript along with it so in this case you'll get the interpreter you will get some kind of formal verification tool sets out of K and whoever is the person that is sort

of updating the JavaScript language can just update the semantics of JavaScript in K and in etosha tools at all the tools will attack it automatically and correct by construction which again I want to reiterate that this is not how things are done in most other approaches most other approaches you develop a model checker for JavaScript or develop a program verified for JavaScript or you develop a simulation engine for JavaScript we do not want that because we believe that is a huge amount of effort and the waste of talent literally there are many PhD

students of top universities who do just that for their PhD they define disabilities an engine for JavaScript or a deductive program verifier for JavaScript and and and and so that has lots of disadvantages not only duplication of work because each tool for JavaScript or Java or C let's take model is a model checkers implement the same algorithm over and over and over again just for a slightly different language or for slightly different infrastructure configuration syntax and so on so we believe firmly that these two should be implemented once and for all if I implement the model checker I won't implement a model checker once and for all and then to take the programming

language is input and never touch the model checker right so is that if you think like if you end programming languages and K or M the same odd K K is taken so in programming languages and M let's say tools that you might be interested in like like an interpreter or a compiler symbolic execution engine model checker symbolic model checking deductive program very fair right so n languages and M tools you have n times M combinations right and and people implemented such combinations for different languages with different tools not only published papers it's easy to publish papers behind er that this varies it's a lot easier to publish a

paper than to develop something that lasts and let's watch it is about compete this connection between languages and tools under tools could be implemented once and for all as efficiently as possible and by the way everything we do is open source and we encourage the community to contribute right so then everybody can contribute to the model check addressed to make it faster and faster and faster and better and better and better and then completely separated we define language semantics that are passed as input to all these tools right and I can use exactly the same with a checker tool with Java or with JavaScript all with EVM they take in virtual machine or we here or with any other language it literally should not matter at all

and if it matters then something needs to be fixed because things should be done complete language independently and that's the philosophy of the K framework and the tool implementation is done in the spirit and the foundation the load the mathematics everything is done in this in the spirit it's a matter of engineering now to just make it work all the way through and there is a lot of interest now from the blockchain community which is great because together we can make it happen so give us a sense of why the blockchain community is interested in K and why is starting to be subtraction for the student blocks in space I think the the

blockchain faces challenges that were not there before like imagine imagine that you have a C program in your car running in one of the electronic control units in your car right even if that has a bug nobody knows the code and nobody knows how to attack it right but on the blockchain everybody sees the code and if the code can be exploited if there is a bug that can be attacked somebody with somewhere so there is a huge huge incentive on all sides now to get his programs right correct secure and what does it mean for a program to be secured or correct what does it mean

for a stream to be a program should see we get back to the same questions you need a formal semantics of a programming language once you have formal semantics you can say what the program is once know what you want to know what a program is you can start reasoning about the program and you can prove properties about it and then I can give you an actual mathematical proof that this program is secure but you can still try to attack it but the likelihood to attack a program has been through secure is it's much much lower then then then a program that has been just written and hoped to be to be

secured it doesn't mean the program's all verified programs are correct sometimes they may have issues because the specifications may be wrong the programming languages may have flaws but actually we have verified many smart contracts as part of prob you saw it on our webpage ratification comm we have a smart contract service that we offers the mascot a verification service and we do verify smart contracts and we verify lots of smart contracts and there is not a single smart product that we verified which was flawless as we found little issues in every single one of them and and that's because simply because what we'll execute is with the formal semantics there is no behavior missed

you see everything with the formal semantics of the language provided you have a correct formal semantics of the language that's that's another question is this the right semantics to the language and some languages are just too complex to you know sometimes you may wonder if you capture the right right mathematical model of the language because the remedy is too complex sometimes not even the inventors of the language know exactly what they meant you know certain construction so essentially in the future that the K framework enables is so today when I let's say when I write a smart contract what I what I want out of my smart contract is a high degree of

assurance that the program will behave a certain way in all conditions right yes so I want that that form of assurance and I found I want that form of assurance that that smart contract will is always going to give that money to my descendants and nobody else right now now there is like lots of places where things can go wrong in getting that form of assurance the first is the first is of course like human error right so so there's some developer that is developing the contract and they can make an error in its implementation but then of course this the second kind of

error could be that the developer is developing his in solidity and their solidity has versions this is 0.4 dot 2 and this point 4.3 and stuff so the developer developed using pot using 0.4 dot - but actually when we compiled it down to bytecode somebody ended up using the next version yes point 4.3 and that caused a bug of some kind or she'll be the compiler is a bug in itself that's the third kind you may think that the program does what you think that it does according to the quality code but when he gets down to the EVM it would be something completely different you know

because if you have has all kinds of restrictions like the stack the stack is a finite bounded size and that size is not visible in authority program they may think that everything is alright but actually it's not or you may have an overflow or the compiler may change the order in which the originally is being done and an overflow that was not there before occurs in the binary that he generated so all sorts of errors that can happen so I think reading the formal semantics will not prevent you from making the human errors right if you type in a wrong account number or transfer your money okay that's a human error right but it will at least avoid the stupid errors the errors that should not happen unexpected errors that are out of your control as a as a human eye

so those should not happen I should not have a combination error you know I should not have an error due to an overflow because you know some shortcuts were taken somewhere in the implementation of the language or in the design of the whole language and a shortcut could be not having a semantics at all I saw some people you know just saying let's not waste time doing the semantics and then it is not clear what what what the language is supposed to do and you may have two different teams implementing the language differently because they like like the hippos are what we see but there are lots of sheep programs that you compile them with GCC you get one result to compile it with clang get another restart you compile it with the intern you see see the Intel

compiler we get another result that's ridiculous right if you think about it imagine that imagine the same thing happening with yours more contract right right does not contract we have two different behaviors depending which you know which compilers were used so this is how like um you so do you use like the equivalency checker to like verify the compiler especially where like you could like you can you can check you have solidity compar to find in k and then you have the EVM bytecode defined in K and it's the idea that you can use you can like check to make sure that the solidity code is equivalent to the out compiled EVM bytecode so guys before I answer this let me tell you that I'm

very impressed with your knowledge your questions are so deep and nice so it's a pleasure literally a pleasure talking to you so all right so two approaches here one is to do the human eyes checking that you mentioned right so you have a separate you have a they say a language validity and you have a target low level them with icd-10 in virtual machine EVM right so you can have a semantics of solidity you have a semantics of the EVM as a matter of fact we talk about semantics of the EVM and we are in the process of completing the semantics of solidity once you have the two formal semantics now you can take a program translate it and you can prove that that program duration of program is equivalent the source to the target program based on the semantics of mathematical semantics of the two

languages so first of all notice that this question itself what does it mean for the original soy tea program to be equivalent to the EVM program this question cannot even be posed it doesn't even make sense without formal semantics of the two languages right what does it mean for something to be a program what does it mean to be Cuban to another program not to the finished of the languages but reached approach number one right where you can take up to 70 set up two languages a program and you can prove the program equivalent the original program accruing to the target program and it is called translation validation actually you know in formal methods another approach which is the one we're employing right now actually in our smart contract verification business

around of Education comm is to take the compiler completely out of the picture right so I don't care we don't here literally what you meant in your soluti code we verify the binary that generated EVM binary I don't even care what compiler you use what compiler version you use nothing we just take the final binary and the trick here is to come up with the right specifications right because whenever you verify a program you verify it against some formal specification so what we do actually talk to developers we sit down with developers actually right now we have two developers from that hub here so it's always great to work with people

who actually develop this code right so we meet with developers and we talk to them and we sit down hours days until we agree on what they meant in order to come up with the right formal specifications we haven't helped them come up with the formal specifications if needed and then once the formal specifications we verify the objective binary against those formal specifications again if we find any discrepancy any behavior that was not captured by the formal specifications we immediately report it to them and then we map those bugs back to the original solidity code because in the end we have to give them error messages ready to the authority code and I said we in everything that we verify so far we found some flaws in one way or another

most of them related to overflows or missing or implicit assumptions there's another thing people thought that the program does something but it does that thing only under additional assumptions that they didn't really capture in any way and then they made additional checks in the program to make sure that those things we need hold those assumptions so yes so you can verify compilers you can validate compilers you can do translation validation or you can verify directly the generated binary which is what we do right now and we can afford to do that because smart contracts are still relatively small but it will be very hard to do that with the flight software at NASA or Boeing right because

those have already millions of lines of C and then when you compile them to binary did that huge and it's very hard to reason about those but for smart contracts is relatively you able to verify directly though the binary it's the safest way to go anyway so I wouldn't be able to for example like you know let's say we have two major aetherium client implementations get and parity and we just saw like this week there was a bug in parity that would have caused it to like fork from gas right yeah but the issue is that these code that you know these client code bases are much much larger than smart contract so it wouldn't be possible right for now at least to use like equivalency checkers to check to make sure client implementations are the same

it should be possible it should be possible of course it's a matter of effort and resources so sometimes so right now for example we are verifying the Kasper implementation for datum foundation we have a security grant with them and the program is only several hundred lines of VIPRE and it still takes about two days to run all the proofs for all the properties that we want to verify right so let's say a thousand lines of code and it takes two days try to verify completely but it's all completely automatic once we write the properties it's all complete automatic so you can imagine if you have a

program that is a hundred thousand lines in you know then we like C or Java there to take a lot of time unless unless you know you help it you can provide lemmas you can you know give hints and and help it but then it's less automatic and it's it's more work for users so I would say you know first of all I think all smart contracts should be verifiable should be verified actually these days the most I would say the most insane that that you know people bet their money on smart contracts that are not verified because you know if any flaw is there then then

you know things can can go completely wrong and it's not that hard to verify the smart contracts yes it's harder to verify larger programs particularly you know consensus algorithms and so on those are very very hard to get right and to verify very hard to even specify what what I think what means for them to be secured and correct that is more contract themselves they they are very low hanging fruit we can do it right now and we should be because a community so last week on a presenter we had silica come on and talk about their skilar language and their school language that they're building is like they're designing it to be very the designing it for compilation to talk at some point

and for now they're doing all of the translation to cop by hand and in the end they want to get it to compile to is the idea with K is that instead of all of these different smart contracting languages compiling to Fidan how to compile clock they just have to specify in K and the ideas that K will then be able to compile to contact some point and is that possible already is there already a clock backing we have a back-end and more in more interesting lecture you can take the the cop proofs and translate them into proofs in the logic and Orion K matching logic so in some sense you can take proofing into precinct a actually and that is not surprising because it is always the case that you can go between

different semantics frameworks once once you have something defined ridiculously mathematically then you can translate from another it was mathematically defined thing to it and become fourth so it doesn't mean that one is more powerful than the other in the end they are all powerful but I would say the difference is that we do not translate things to K all right so we do not take a language and translate it to K in order to reason about it we actually construct the language define the language in K without the translation all right as we discussed we define the syntax and that gives the granularity and then you add the rules that work directly over the syntax of your language so you can basically step by

step can actually we do have a step command right you can push step step step step and you execute the program exactly in its original syntax using the case the case Ematic rules and our logic the logic underlying here allows you to prove properties about the program directly of the K level without translating to any other formalism yes I understand it's very tempting to take a language and translate it to coke but then you have to start worrying about your translation itself why is my translation correct what people do also very frequent is to define languages in code directly the same way we define them in K then you find them in code right and sometimes

those semantics executable so they can get an interpreter out of them as well and then they can also do this and in using so when they do that the two approaches are very similar but keep in mind that in K we have a lot other tools not only approve all right so Koch is an interactive proven so you have to interact with it and prove things we can we can also do symbolic execution we can do symbolic model checking bonded model checking there are lots of tools specialized for languages book is not really specialized for programming languages focus is a proof assistant for any proofs in any mathematical theory it's a lot more general and there is a price to pay for that I guess like I'd like to get a sense of

what the future looks like when a lot of smart contract language developers adopt the K framework to define their languages so I think of course like one of the differences is pretty officer today salinities is developed by christian wreath whistler and his team and and in the future the way their workflow changes is they define solidity semantics of solidity in k and whenever they want to issue an update they just issue an update to the semantics in k and that's it k will take care of making a compiler for it interpreter all of the formal analysis tools etc yes now if I'm a developer

that's writing in solidity hmm I need to specify what version of solidity I'm using and I'll get the semantics the K semantics of solidity and when I write a program I can use the formal verification tools that come out of K to prove things about my program yes and now as a developer whenever like solidity upgrades I can also sort of upgrade to the new version of solidity and have the proofs of my software in there the compiler and everything all the tools for the new version yes so the way I envision is is K to be like universal language for the blockchain

right in which you find your languages these that solidity various versions of salinity beaded Viper Pluto's whatever language you want to write smart contractive high-level language I say n even the lower-level languages well to know whatever level lower level languages there is another study which I'll talk about later but now let's talk about high level languages alright so now I would like to have these semantics of languages themselves be somewhere in the blockchain ok because I want that to be fixed nobody can touch a semantics once I have it has a unique ID version number three point two point seven and it's fixed I don't want that to be touched

right so then we can refer to it on the blockchain and then we can generate all the tools from it and then you can help us not contract verified and I want to go one step further not only verify the smart contract but to have an actual proof of correctness of the smart contract and that proof itself or a hash of it right to be also stored on a blockchain there is not only that I have my smart contract on the blockchain but I also have approved why the expert product is correct and that proof is checkable by you or any third party in a way that you don't have to trust the key framework because the key frame work like any other framework skin can have bugs itself Oh head bombs right people proof false with

coke right so so so that's an avoidable but what but what we'd like to do is to use these tools this program verified like like like like like the keyframe of Rama to search for a proof once we have the proof we should be able to get the proof object that is completely checkable independently of K and I want to attach that proof object to my smart contract and this way you can imagine having smart contract on the blockchain together we certificate where any certificate hey right said my my spa contract is correct missing this is the proof so don't even think about attacking it because it's been proved correct and it is the proof but if you believe that this is the specification they say they take on ERC

20 contra right you have one year c a specification for your c 20 that is public everybody agrees that yes that is the foremost discussion and share C 20 and now you prove that a smart contract implements an RC 20 end of story it's correct I have a proof that is checkable I don't care how that prefer generated whether with care or something else I don't care there is a fixed semantics of the language there is a fixed proof and those can be checked and you can even imagine checking these proofs as a service on the blockchain and and you don't even know you know have to worry about it as a user of a smart contract about K or anything like that you already have like you know okay that is it's green that contract is green it's been proved correct but of

course in order for this to happen I mean there is a lot work afford to be done you know to generate proof objects we don't generate two objects yet also the compilers which they are still working on compilers from the semantics we call the somatic space compilation that's not yet there some research to be done or to improve performance so is this what this is a 20k project is because like so the ERC 20 is just like an interface right it's just yes it's basically just syntax it's saying this is what a function should look like and then so this is C 20k project was adding semantics like not only is this a syntax where this is how well it should do this

is what a send a transfer function looks like what does so we were we were asked we've been asked to verify samia's he 20 tokens using our semantics of the Italian virtual machine and we verified some properties but we did not know exactly what what does it mean for something to be our C 20 compliant right so yes we looked over the syntax over this API and there are lots of words describing what they P is supposed to do but that's not rigorous enough in order to get proof that so then in here C 20k we formalized the ERC 20 intended protocol completely to the last detail all the cases considered or all 13 different rules

semantic rules that were hidden in all the text in GRC 20 in formal description and now we have a specification we know what you are see 20 is from a mathematical point of view and now if somebody gives me a token an implementation let's say the EVM level and clicks NERC 20 I cannot take it and automatically check it against the RC 20k specification and if it has any flaws then those would be found and reported given that you know many of our listeners are probably familiar with like a RC 20 you could you maybe share whether any like hidden things you notice in the ERC 20 like because any any gotchas that may have like not been

noticed unless we went through this formal specification yes so so people typically don't think of transferring from you to yourself or when you go transfer from so you can transfer from A to B and you can be the color see sometimes a PLC can be the same entity right so what if what if you transfer from yourself to yourself and you give yourself your language to transfer right so sometimes it's interesting that the order of operations matters right whether you first deduct the value from the from the account for me to transfer and then you add the value you know to the to account versus if you add the two

first and then we deduct the value from the from account so these are completely orthogonal operations provided that the totems are different from an two but if they are the same account the order matters because one of them will run you into an over an overflow the other one will not so you may prevent an overflow by doing these operations in the right order and and actually depending on which order you do these operations you can have two different specifications of DRC 20 and you have to comply with one or the other which is a bit inconvenient but but yeah so this was the totally unexpected behavior that when I transfer from yourself to yourself and we found

lots of implementations where people sometimes refer to as the value first and then deduct it and others who prefer deduct the value from from the balance of the from account and then they they add it to the other one and and and now you can have one case because that's what typically you know errors are in corner cases you have this corner case when you transfer from yourself to yourself and if you don't you prevent things properly you may even be in a special review generate new tokens by transferring from yourself to yourself you generate new tokens which is crazy I think like we we are we are running out of time but like one of the last topics we would like to cover is your partnership with IO HK you work for the

car Dino project so there you have created something which is called the K EVM right so walk us through what ki EVM is and how it will be used in Cardinal so K EVM is a is a formal semantics of the EVM the same like the ERC 20k right so we formalize the entire Italian virtual machine in the K framework and that gives us an interpreter basically implementation of the virtual machine and that is fast enough it's only like an order of magnitude slower than the C++ reference implementation and in the eye which K actually deployed these virtual machines are incomplete automatically from the formal specification on a test net a couple of

weeks ago and and the players do the same with ela which is an even you know the next generation of virtual machine for for the blockchain that we design together without H K and yeah so so first of all so it's a formal semantics of a low-level machine and you can use it to execute smart contracts the same way you use the EVM implementation in C++ right to to run smart contracts on a blockchain however you can also use it to verify smart contract to prove for contract rate which is exactly what we use to verify all this year C 20 compliance I was talking about all right so the factor K VM is and and and and it

is very tempting to deploy on a Desna such such such such a virtual machine because it is essentially correct struction there is nothing to prove about it right so you mentioned before Sonny that that you know you have these complex implementations and how do you know whether they are correct if there are large and so on so the actual EVM is large that's a large piece of software right but if you generate it completely automatically from the formal specification in a way that is makes it correct by construction now you have you know high confidence that you will not have bugs in that part of the of the system but so you did mention that it's like almost an order of magnitude slower

than the our C++ reference implementation so would it be possible instead of and like instead of using it as the base client like the client of everyone uses to have a test net or network that's entirely KVM what if it was used more as the reference client or like what I call it like I think till dying I am sure your from it definitely can be used and actually if you go to jello paper org we have we deployed actually we have a paper meant to replace the yellow paper right which which has which is a reference implementation of the EVM basically yes protected from the semantics however

however we are working on a project now also with with I which K we want to generate a faster back-end for k when LLVM back-end so we are going to translate automatically the semantics into LLVM and we expect that to be an order of magnitude faster and once it happens we'll be able to actually generate you know comparable in performance virtual machine implementations from formal semantics and then then you may wonder why should I even bother implementing a virtual machine if I can generally talk too much before the formal specification correct by construction and it has comparable performance why why should i implement

why should I take the risk mean don't use bugs if if I don't have to essentially professor is it correct to think like so today you see a lot of different projects in this space where these projects set out to implement their own virtual machine and a language that compiles down to their virtual machine and then this language helps in formal verification in a particular way yeah and so this is this is the story behind tezo's this is the story behind scalar which was the last project we did this is there's another called Zen cache or something like that so Zen project

that's also doing something similar and essentially the scale approach with Cardno could be like one approach that like overshadows and solves the problems that these projects are trying to try to solve essentially in the K approach what would happen I don't know if it solves all the problems but it solves one problem which is that you can write or smart contract in any programming language for which you have a formal semantics exactly so once this is running on Cardinal so let's say the the programming language of Essos Nicholson was was interesting developers wanted to use it somebody could just Express the

formal semantics of mickelson inkay yes and then and then developers can write a smart contract in Mickelson and executed in kvie via a VM or ela or y la hora but but in order for that to happen we have to still finalize this project the we're working together with AI which K on which is called cymatics based compilation which is the following we give me a language semantics and I give you a compiler for the Glenridge and the compiler is specific a translator from your language to a low-level language which we plan to be ELN ok so yeah there would be this new virtual machine it's an EVM like virtual machine low-level language it's actually a combination of

EVM and LLVM you may have heard of LLVM so if it's an energy for the blockchain try to design this language together with average K and and and what we want to do is to take any language which you have a case semantics and automatically generate a compiler for that language to enn alright so if if you suppose it to have you like JavaScript suppose right you write this you write your smart contract using javascript and as soon as far as you have a semantics for JavaScript in K you can push the button and translate automatically correct by construction your JavaScript smart contract into your a and then run it on the auto watch preaching array get Yin a

VM so everything is correct entire stack right entire Python is correct there is nothing no code that needs to be verified by hand anymore because the entire thing is either generated automatically from the or is for mathematics so you with the yell a I noticed you guys also have a K webassembly system as well and so what were some of the reasoning behind the building of the other because I know web assembly is also very similar and closely tied to LLVM yeah so what were some of the benefits like thought process of building y la when you're

looking at like what existing web assembly and EBM and stuff so you may know that LLVM and then vm has been created university of illinois is a professor in my department Vikram Ave was behind behind LLVM so we have a lot of legacy here at UIC with LLVM and we love LLVM and and particularly one thing that we like about it VM is all this optimization the LLVM optimize optimization pipeline right we take a little vm program to another in vm program which is better right from some points of view or by some metrics and then you take that to another religion program and to knowledge so keep transforming the program until you get the final program that you're

happy with and janitor's a - not if code so we didn't like this approach because in particular you can imagine that you can take any high level programming language translate it quickly to LA to LA let's say right because la is like an LVN jelly's LLVM for the blockchain think of it that way I translate from that high level languages in JavaScript to ela and then you go from here to here Twitter to improve the gas metric let's say or to improve the size of the code or you know you have some some some sixth improve and we can use many of the ideas that have already been developed by the LLVM community and that's what we'd like to build up when we like to build up on what his legacy and all the tooling that has been developed around

the LLVM project well if we did the same for web assembly then we would have to reinvent probably many of the of the of these techniques for for Reb assembly and while do it when we already know that this work for LLVM and but yeah so as you may know it should we define the semantics Inc all these three right we defined the KVM we define the semantics of webassembly and we are still defining it now so one of our one of my students Everett Hildebrand he's actually also working for the Italian Foundation and he's defining the webassembly in k as well and then we have the other that we defined for for for IOH K which I which K so it's not like we favor one over the

others actually to be honest I I favor yellow over if here because we really design the other you know you know with the explicit objective to avoid some of the problems that we learned while we formalized EVM and but in between what was sembly and Elia I've done I don't think there is any any big you know differences in terms of you know one should be definitely better than the other or one is better than the other and as a developer of the keyframe or to be honest I would like all the flowers to bloom so the K framework allows all of these to leave at the same time and once you have semantics based compilation you can just change the target language and then you can go from

any language to any vm right I can go from JavaScript to to y la or to JavaScript from JavaScript to EDM or from JavaScript to Watson although should be possible because because of the way the code is generated it's not hard to change the backend of the of the code generator and that's for execution but then the result always the verification aspect right so having formal semantics for all of these both for the languages and for the VMS allows you to have no code left which is not formally verified which is my dream that's what I'd like to see in the blockchain space is like all the smart contracts to be formally verified sounds sounds great professor I mean I my sense is that the K framework is the general the most general solution to all

of these small specific problems that many of these blockchain projects are trying to solve by inventing their own languages and their own virtual machines and and things like that and um I'm looking forward to what change ke brings in so please don't get me wrong but I'm not saying that these languages are not great I think all of these languages adventures are great and they must be done we have to come up with better languages for Damascus mark on track with better virtual machines but what I would like to encourage everybody to do is to have formal sumati for all of these and then to have these generic tools that allow you to easily change the language or the VM and still have all the tooling around as opposed to implementing reinventing the wheel over

and over and over again which is what we see a lot happening at least in the academic community cool okay so that brings us to the end of the show to our listeners thank you so much for joining us we release new episodes of represent a Bitcoin every Monday or Tuesday Thank You professor for being a guest on this podcast we enjoyed the conversation a lot thank you guys great questions I'm very impressed you really understand well the key framework that means that we did our job well so you really it's amazing how you how keep your questions are and right to the point your videos and documentation works really good like I'd

walk to watch through some of your tutorials and stuff those were very helpful excellent thank you guys so far listeners if you're tuning in for the first time you can subscribe to the show on iTunes SoundCloud or your favorite podcast app for iOS and Android you can also watch a video version of this particular show on YouTube at youtube.com slash epicenter Bitcoin recently we have also started a gator community where you can chat with us the hosts and other members of the epicentre community the link is epicenter door TV slash gator we look forward to catch up with you there we always welcome reviews of our show it hit it helps it it gives us

feedback and allows us to improve it keeps us going and it helps other people discover every Center so please leave us a review on iTunes and we look forward to catch you [Music] [Music]