Hashing It Out
Hashing It Out

Episode 100 · 1 year ago

Hashing It Out #100-Chris and Jay of REACH

ABOUT THIS EPISODE

On the 100th episode of Hashing it Out Corey and John speak to Chris and Jay of Reach. Reach is a platform seeking to develop a programming language for the easiest development of smart contracts and dapps within the cryptocurrency ecosystem. 

Links: Reach

Welcome to hashing it out, a podcast where we talked to the tech innovators behind blocked in infrastructure and decentralized networks. We dive into the weeds to get at why and how people build this technology the problems they face along the way. Come listen and learn from the best in the business so you can join their ranks. All right, y'all, welcome back to hash it out episode one hundred. It's been a while. We've been gone for a while since the New Year because we're busy, but we're back and for episode one hundred, big zero zero, as always, on your host, Dr Corey Petty, Cohost Day, John Marlin. Say what's up man, what's up man? What's up man? And today's episode we're going to be interviewing reach. We have Christopher, or Chris and Jay for reach to discuss a new way to build decentralized applications or applications in general. So we'll go a kind of dive into the weeds as to why this approach may be better then the standard way most people are building decent draize applications and how it gets used today and where it's going. So, Chris, Jay, what't you start off by introducing yourselves. Chris, go ahead. My name is Chris Winner. I'm a CEO of reach. My I started out long time ago, twenty years ago, as an engineer, and about ten years ago I abandoned it to be on the business side. So it's been the last ten years in management and entrepreneurship and been running reach now for about, you know, about a year and a half, a little bit, maybe a little bit more than that now. But Jay, my name is Jay McCarthy. I'm the CTEO of reach and I'm also a associate professor at the University of Massachusetts will and I've been doing research in programming languages and formal verification and carmographic protocols for most of my career, since getting my PhD at Brown back in the early S. Doctor Chamber Carthy, I apologize for that one. Use The moniker when it's so it's appropriate and that in that case it's in a perfect conversation. We've had quite a few people on the show discussing static analysis, from will verification security. You can programming language for that matter. What makes reach different? So how kind I I would like to explain this is go back to me three years ago. All three years ago, we're building a block Skame, blockchain scaling solution, and we built out a prototype of rate some money and what we them. We were got to the point of the KAYS. Time to find developers. So we started hunting for developers, going to conferences and started seeing started seeing the same faces over and over again. We're trying to find out. It was difficult to find those developers and we thought that was really weird because at that point we drank the cool aid. We knew blockchain of this future, but they're just no developers out there. So start to ask and developers questions. We asked why, why are you not developing in blockchain? You know there's twenty, thirty million of you out there. What's happening? And through surveys, through conversations, there's three things that kept surve for saying. Number One, blockchain development, which is too difficult. They are finding that dropping down to the level of the state machine and program and a state machine was just not something they were used to. So it was completely different type of paradigm that they need you to learn to be able to build blockchain applications. And not only is it was it actually more difficult, but because it was a lower level it took a lot longer and developers like that instant gratification. They'd like to be able to sit down, build something and have something, but with blockchain they were sitting down building something and...

...nothing like. It was just taken way too long to actually build anything. So they're running out of steam. Second thing that came up is just the cost of blockchain development and the cost of blocking development came in multiple different ways. Number one, if they wanted to build a team around them. A blockchain developer, you know, makes two hundred fifty an hour. It's a very difficult to actually find to developers to join them Ountin team. Say that if they they found the team, they found the money to actually pay the pay the team or and Syndervis them in some other way. Once they actually built the applications, now they have to get audits and that cost tens of thousand dollars and a lot of times they'll have to do that with multiple difference auditing companies and every single time to change their code. So that was really costing. And the final thing is that they see these companies that build the team get the audits and are still losing a hundreds of million dollars because I'm bad code. So they're looking at it and saying, you know what this is, this might be a little bit too early for us to come in some costing a lot of money to actually take that risk. WHY WOULD I change? And then the final thing is that blockchain in general is very tribal. There's really no such thing as a blockchain developer. There's an a theorem developer and LGARND developer and a car downa developer and but there's no such thing as a blockchain developer, and that's because the skill set is just so different. It's very difficult for them to help each other. And not only is it so different that they don't can't help each other, but it's actually very toxic. My chain is the best chain. You're an idiot for picking your chain and and it's kind of regular. Developers look at that and say, you know, why would I deal with that? So those are the three real major pillars that were finding why blockchain developers weren't coming into the space. So we knew that we had actually fixed that problem and we could do a one of two ways. We could build a development tool that focuses on one of those aspects and iterates on how things are currently done. This is, you know, the teams at truffle and hard hat are built the the team that built hard hats. Myth. Relax, this is the direction, let the way, and they did a lot of good work, but they built their tool on the on the foundation of how blockchain is and the truth of it is that blockchain development is so hard and bad that making something a little bit better isn't good enough. It isn't a good enough to actually make a difference. So we gave ourselves to the challenge of saying, okay, what would blockchain development look like if it was a hundred times easier, hundred times better? And the answer came really with is what reach came from the idea of actually building a platform, a central hub, a central way to actually build blockchain applications that took care of everything, that change the actual paradigm of what blockchain development is to actually make it at the hundred times better. So what reach does exactly is it provides a programming language, which the region language, that raises the level of abstraction, allows for developers to code at the level of the participant rather than level of programing of state machine, because it's a much higher level. It's actually much, much shorter and much more efficient to code, so developers can actually get down and actually build applications very quickly. Give you a real world use case is that we're currently in the process of rewriting UN swap in reach. Currently, that is the reach application is two hundred fifty lines of code, which is much, much more, much shorter than what the you know swap contracts and the middleware is now. Director really prove the the use case of you know reaches actually easier, we decided to put our newest developer on it. We said we hired him a little over a month ago and said Hey, we want you to build unic swap using reach, and before we hired them he never even saw what bought new...

...a block chain was before us. So we took it a full sec developer and we test them with building u swap and he rebuilt you know swap from scratch with reachs in two hundred and fifty lines of code and we know, with minimal help from us. So we knew that we checked the box of making it easier to develop. The next thing that we wanted, you know, make sure that we fixed it's the safety aspect, which I'm guessing we're probably talked quite a bit on on this podcast about that, is that we wanted to make sure that the the the output is correct on complex compilation and there's a thing out there called form of verification which mathematically guarantees that the output is correct. But traditionally, you know, runtime verification. Many companies out there that formally verify will spend time and generating and entire a model to actually prove that the actual code is is correct and they have to actually develop this all out by hand. It's very expensive, it is very time consuming and it really requires the developer, after it's done, to maintain a speck and maintain their code at the same time. So it's super important. But traditional developers really don't know how to do that. But what reach does is it automatically, formally very generates the formal proofs through the compilation process. So allows for the developers to just drop in assertions into their code and it mathematically proves that the code is correct just through compilation. So we know that we made it so the developers can actually build safer applications in the final thing that we did is we're unifying blockchain development. We've abstracted the actual blockchain, blockchains themselves, the protocols themselves, away and make it so that developer can actually write the application and launched on an any chain without having to actually change their code, as the code at all. You know, this is beneficial. If a developer wants to launch your application multiple chains, that's great, but that's not really the true value. The true value is that any developer can help any developer, no matter what chain that their launched on. We already see in our community that's Algor and developers are helping etherium developers, which are helping Cardano developers, and they don't know it. They just answering questions, they're they're making, you know, helping building these APPs and they don't even ask where do they launching it, because it doesn't matter. And we remove that toxicity from the entire industry and made it like, you know, unify to all inner one banner, which is really exciting. So that's kind of like where why we're actually passing about. This is why we actually, you know, get up in the morning to to actually work our asses off. But yeah, that's so. That's a that's reach in a nutshell. Jay kind seem to add of that. You know, your original question that you asked was, you know, what makes reach different, and I think that Chris touched on a lot of those things. So we when you write a reach program your program or your programming at a different level of abstraction from, you say, the traditional solidity development. Like if we take like a typical solidity program, the way that you think about it is you say, I'm going to have some particular state on the blockchain and then what I'm going to do is I'm going to write down a bunch of different methods that modify that state, and when you're writing these methods, you have to think about when you would like to enable those transitions to be allowed or not. This is what Chris meant when he said that you program with the level of the state machine, because essentially what you're doing is you're specifying, you know, the state of your the state of your contract, and then each one of the methods is basically like an Arrow modifying that state. And a major problem that comes up is that you have to spend a lot of time trying to decide when...

...to enable different transitions. But you're slowly. Program doesn't actually say anything about like what order the should happen in, what the people who actually use the program should be doing, and those things have to be recovered when you're doing a verification of a smart contract, because otherwise you'll just basically have to reason about every possible interleaving of all the methods, and that is like infeasibly large, right because it's an infinitely large space. So you can't actually exhaustively explore all of them. So you're limited by doing something like bounded model checking. But when you read a reach program you actually include those details about what the end points do, and by specifying what the endpoints do, we inside the reach compiler can derive what the state of your program has to be and derive what state transitions should be possible, and then that's what we compile. So, like a technical level, that is like the key thing that's different. I suppose that there's one other thing that's quite different from a program like a programming language like solidity and reach, which is that in reach, because we want to enable automatic verification, we need to remove features from the programming language that we can't dispatch without human intervention. So what that means is that basically there are some kinds of programs that you can't write because we want to do automatic verification. So, just as a little example of that, in slidity you could write by hand a whow loop that had a really complicated termination condition to that you know that you've thought about on paper or something like that, why it's going to terminate and why it's not going to have infinite gas costs. But when you program in reach, we limit the kinds of, you know, wow loops that you can write two ones that we can guarantee will terminate, such as the tiny example, or essentially a non turn complete language. And kind of our hypothesis is that the vast majority of blockchain programs will fit inside of this restricted language, because, of course, the alternative is that you would submit a transaction that could use arbitrarily large amounts of gas. so by making the language be turn in complete in this way, we actually have predicable gas costs. John Got Causes, I got a lot. Yeah, just is like, how's it going? So, like that's a bit of a bit of a challenge, I guess. Like like UK, you got you got an active community's comby between Algorithm and etherium and even Cardano devs. I currently there are some. But so, I mean, but, but I think like it's, I don't know, like solidity is like so bad, it's the best. Like I worse is worse, is better. Just keeps playing out for for lack of like you know what, for better or worse, worse is better. So how are you going to overcome that like initial traction of solidity and just like get the deav mind share? It's a great question and we took a big risk. The big risk was by building and overall platform. Takes a lot of time and it takes a lot of time without actually getting the feedback from the users. So we took about a year and a half, a little over, a little over a year to actually build out the reach platform before we could even get any users. But as soon as we actually did and we open the doors and the launch our documentation, that wasn't less less September. Since then we've grown by ten to twenty percent every single week. Last last week alone we added fifty four...

...developers to our platform. This is not, you know, Fitch for community members, this is actually developers that are building and compiling applications, and so I how are you counting that then, like like mpm in souls or something? So No, so what it is is that's if you because it's a compiler, you'd conduct you download the compiler from doctor and we can track unique doctor IDs that download from doctor. Sure, and in the way that it's done is that it doesn't actually go through that process and less you go through and and compile the actual your application. So we know that this is not people that just downloaded. This is people that are using and actually being on board and building applications. So weird most of those developers are coming are actually from those traditional developers. It's it's pretty surprising how easy it is to actually gain developers from the real world when you make it accessible. We're not we're not pulling from the existing blockchain community because, you know, it's a few thousand people. We're pulling from tens of millions developers in the world and they're coming in. And I mean we have a we're running a bounty hack proper program right now and one of our participants is eleven year old kid has gone through the in tutorial and is actually building a was it a wager based tic tech to application that's fully decentralized? He is eleven years old. That's how we're actually growing is that's where we've made blocking development easy. So you do formal verification on the language to make sure that what I write in reach does what it's supposed to do and nothing else. Are these based on the assertions that I put under the code? How is that guarantee carried down? It's the compilation of a bunch of different languages, whether it be etherium, all Grand Cardna like the those are all drastically different implementations of blockchain that have different foot guns. How how are you taking the guarantees and making sure that the compilation process carries those guarantees all the way down into them being put on to some blockchain and the middleware around them? Yeah, so the gold standard of doing something like this would be a verified compiler. So basically what a verified compiler is is a theorem of the form. For all input programs there exist and output program where the meaning of the input program is equal to the meaning of the output program. And you could write your compiler like this and you would then know that the semantics of the input program was respected by the semantics of the output program. Such a gold standard. Pretty much the only compiler that exists that works this way is called concert. It's written and Cock and it is it's a C compiler that targets the basically what it does is it's input is a subset of C and it's output, as I believe, it targets arm and x six and some other micro control. I forget what it is though, but anyways, that would be the gold standard. For my Ph d dissertation, I wrote such a verified compiler for a language that's very similar to reach. That where my input language was, you know, my unique language called WPPL, and the output language was Okamel, and so I use a semantics for oakaml to prove that it was, you know, correct compiler. So anyways, so that's that's sort of what the gold standard would be. We don't do that. We'd like to do that eventually, but but we don't do that and really nobody does that because it's extremely difficult to do. The sort of the next best option is to do what you might call output validation. So the idea of output validation is is that, rather...

...than proving that all outputs are correct, you would prove only that the particular output that you were given was right. So, in other words, rather than proving this for all exists, you would say that for this particular input to your program we would prove that the output and matches its semantics. That would be another good strategy to do to verify the result of a compiler, where what you could do is you could like try to produce that proof automatically. Something like that is also on the road map in the more medium term, than the the gold standard verified compiler, what we do is we instead prove that the that your program in the reach semantics satisfies its properties. And let me sit back for a moment. Like what is the verific what is verification mean? In General? What I verification means is that you have some property, which of course, could be, you know, an and of a whole bunch of different properties that you want to hold about your programs. You can think about that as a function P that takes a program and returns a proposition. And probably you're not proving the thing on the program, you're proving it on its meaning. So, in other words, you would like to be able to prove that the meaning of your program has desirable qualities. And if you had a verified compiler, then when you proved this theorem on your program you would also be proving it on the output program that ultimately ran. And so essentially what we're doing is when we prove your program is right, your program is correct on the reach like your reach program is correct. We're not proving anything about the reach compiler, about the output of the reach compiler. We're not. We're not proving anything about what solidity does. We're not proving anything about what the teel compiler does or it guest does or anything like that. So in that sense the reach compiler becomes part of your trusted computing base in the same way that if you weren't going to use a reach you know boost, Llvm, theslidity compiler, web three, all of this things are in your trusted computing base. So we essentially have the same trusting competing base as normal application development, but we're proving something about the reach program. Now let me sort of compare this to something like like firefly, for instance. So firefly is a tool that run time verification provides for helping you prove things about theoryum programs. Now, I am not an expert on exactly the techniques that fireflies using, so it's possible that I will miss characterize them. I apologize anyone at runtime verification for me doing so. But the general way that it works is that they have a another different implementation of the EVM and this other implementation of the EVM is embedded inside of the theorem proving tool that they use, the k framework, and by having this other implementation of evm it facilitates proving things directly about the byte code. So, in other words, whereas in reach you're proving something about your input program and you then have to trust the things that are downstream, when you were if you were to use firefly, what you would be doing is you don't have to trust solidity, the solidity compiler. Instead, what you do is you take the evm code that you come that comes out of solidity, and then you prove something about that. Now, in the same way that I talked about the for how reaches at a different level of abstraction from solidity, evum bite code is at a further lower level of abstraction from solidity. So this is one of the reasons why it's very challenging to prove things, prove useful properties,...

...about, about smart contracts, if you're directly proving them, about the bite code, and you know, kind of an analogy for you know traditional you know computer science and programming, right, if you if you want to prove something about an algorithm, you'd like to focus on things like, oh well, you know this value must always be in this set. But of course, when this actually gets implemented and let's say a SE library, you're not reasoning any longer about values being inside of sets. Your value, your reasoning about whether or not a particular algorithm for searching, let's say a red black tree will return true, and if you were to prove something about the underlying assembly, you're not even you're not even reasoning anymore about searching red black trees. And said, you're just saying, suppose that I had this soup of memory. Would I be able to prove something about the way that that the way that all the pointers in this heap are structured? And so every time you go down the level of abstraction, the demands on doing verification become much, much harder. And essentially the thing that's wonderful about the firefly tool is that it has a lot of machinery built in for reasoning about those extremely low level programs of evum bite code directly, and it's kind of miraculous that it's possible for people to make any conclusions about what their program does. So anyway. So that was kind of a long explanation for you know what the formal of verification landscape is like and you know, to go back to the beginning. Reaches part of your trusted competing base for now, and we have multiple plans for how to extend the guarantees about reach programs to the actual compilation output, whether that is a for all exist theorem that we can do once in for all, or, in the short run, doing output validation, or should I'd find try rephrase a little bit. You're making sure that developers capable of understanding that what he's writing does what he support, what he thinks it does, at least within the languages writing, and then y'all those experts will spend time making sure that the rest of it can be also proven as best as it can be, depending on where it's being deployed. And, like you said, that the further you get to like bits on a bits, on a machine, the more difficult it is to prove things and the more required expertise, which isn't something you typically want programmers building applications to spend all their time doing, or thinking about for that matter. And you set yourself up at least for developers to get started quickly, making more, to understand more about what they're writing more easily and a future of slowly making sure that what they're writing is more and more security being upon where it's where it's being deployed. Is that a reasonable, like high level summary of what you just said? Yeah, I think that's great and I think that you know, it's useful to emphasize that. You know, because reach does automatic verification. This means that there's no intervention on the part of the user whatsoever in directing the Theorem prover about how it's going to do something. So we don't ask them to choose strategies, we don't ask them to ask the assertions. Yes, the thing about the thing about assertions is the assertions are telling it what to prove, is not telling it how to prove it. Many theorem provers require you, even ones that are quasi automated, like a sale to what they require you to do is when you what you would do is you would stay the theorem and then you would say, prove this theorem using this strategy or maybe using this induction scheme. And we don't require anything like that. And so instead, one of the things that we try to do is you try to make it so that the theorems that you want to prove about your program are always expressed in terms of the program itself, meaning that you can imagine that when you write a reach program, all you do is right the...

...normal program that you would write and you would add assertions just like you would add them if you were writing, you know, like a normal runtime program. Well, where you would you know, if you have an assumption, you would put that assumption in your program and this is sort of standard practice for, you know, good software engineers, where they take their assumptions and they encode them. But of course, when that's compiled, traditionally those assertions become run time checks. But what we do is we dispatch them, you know, at compile time. So by explaining things in terms of the variables and the program and what the program is doing, we lowered the barrier to entry to doing verification. You know, just as an example, you know this eleven year old kid that Chris mentioned earlier. Him and I were talking earlier today about how to prove one of the theorems in his program and you know, he basically had this situation where he assumed that a variable was related to another variable, but actually they had independent origins. So he just had to make sure that he computed the first one as a function, sorry, the second one as a function of the first one and the once you do this, they're now attached and so the the Theorem prover can reason about them automatically. So, you know, they're sort of simple program like ideas that you can use to understand if your programs right and reach as opposed to they are improving logic ideas that you have to bring in. So there's no additional expertise that's required, and that's kind of the the key point. So you're basically saying like you just have to instrument your code with Assertion Ends and crows are generated from that. Yeah, so let's step back a moment, like what is the point of formal verification? The point of formal verification is to know that your program is the program that you hoped it to be. So you come up to a problem and you have in mind some preexisting solution. This is kind of an important thing about programming, right like programming is not a problem solving discipline. Programming is about encoding automated solutions to problems that you already discovered separate from the programming process. So when you walk up to your keyboard, you already have a solution and what you're trying to do is, if you're trying to write that solution down in a way that is automated. Now, what you would like is to know that the program that you wrote actually is the thing that was in your brain before you started programming. And all verification can do is say if two things are equal. Sometimes it doesn't say if one's equally, will say if one is contained that of another one. As an example of this, actually, let me so. So let me stop for before the example. So what that means is is that the only way that a verifier can do anything useful is if it gets you to write your program twice. First you write your program and then second you write the specification of what your program is supposed to do, or you know, maybe not really first or second, but you write you were thromos for love doing this. To ask John. Well, the thing is is that one of the key sort of tools of good verification is to trick the user into writing their program twice without them realizing it. So, as an example of this, when you write a Java program, you are writing two separate programs. You're writing the program once and the values and you're writing the program again in the types. Now the types, when you write in the Java program, they don't in contain all of the information about what your program does. For instance, you'll write like Oh f as a function that takes two integers and returns a third integer. That doesn't say that it's supposed to return five when you give it two and three. It just says that if you give it two integers, a third integer comes out. And so when the Java...

...verification engine, which we just call the Java type system, runs, what it does is it make sure that the value program that you wrote is inside, meaning that its behavior is permissible by the Type Java program that you wrote. And as a programming language gets more as a type system gets more precise, then it becomes more like a formal verification engine and what a formal verification does is it allows you a way of writing down that specification. Okay. So now when we talk about reach, if you just write your reach program and there are no assertions in it at all, at a first glance, that means that you didn't write down a specification. So the reach compile that the re verification does nothing because you didn't tell it what else you were supposed to do. No, existing traditional programmers are already used to the idea that they should write down their assumptions about what values in the program what values variables in the programs have, as assertions, and they think about those as being things that happen at run time. But if they write them done in reach, they now just wrote Don a specification, because, while those things are useful and sort of normal programming to prevent you from going off the rails, they are a way of getting the specification out of the head of the programmer. I would now argue, before you keep keep going like sure what you're talking about when you say programming is more like traditional programming and not like what I think the colloquial term for programming is, which is more like scripting. Like I come A. Maybe it's because I come from Fortran background and so you you specify everything implicit none as the first line of every single fortran program and there's similar there's similar constructs for other languages, and so you have to kind of define memory access to bounds in which things can go atter modernday programming, especially onence modeled like javascript. Tend to not have that concept when learning how to program and and and I think what what's important is that we get back to that concept of teaching people when writing things that deal with money, okay, blockchain, they should be thinking about these things ahead of time, and a language like reach the kind of really pushes you in the direction of doing this and gives you a lot of benefits for doing it. Is it is a generally good thing. I think I agree with you, although I would say that reach is more dynamic e than you might be thinking. So playing around with it, it's very javascripting exactly. So. So if I were to listen to what you said, you might get the impression that, oh, when you write a reach program you have to like declare ahead of time that I'm going to use these ten variables and they have these types and all this sort of thing. But actually reach doesn't work that way. It it's more like it infers things about what your program does. And kind of a way to think about this is like, take Javascript, for instance, or Python. You don't need to, let's say, declare the types of variables because the language implementation is sound, meaning that right before it's going to do something dangerous, it will generate a check to make sure that am I about to add a number and a string? If I'm if I am going to do that, then thrown ever. So essentially, the way that reach works is is that we do almost the same thing, except that, rather than generating a run time check that says, is this thing the right kind of value, we actually generate a new formal verification claim that that thing is the right value. And so what this means is that, even if your program actually contains no assertions, reach will generate assertions for you based on what the program does. And we do these four things that are normal programming,...

...things like adding to values, making sure that they're both numbers, or things like going outside of array axis. Will, you know, double check that it's within bounds. And that is a static check, not a runtime check, but also because it deals with money, we can do things that are sort of unique to the domain smart contracts. An example of this is like the linearity property that says that when tokens go into a contract, they have to be used exactly once, meaning that they cannot be used twice and they can't be used not at all, because if they were, if they were not used, that means that the program would end and then the values would be locked away and you wouldn't be able to get access into me any more. So that's a property that is a general one that should apply to all blockchain programs, that you don't need to write down when you use reach, because we can generate that automatically. As an analogy, you know you wouldn't need to write down that you don't want to have no pointer exceptions when you write a C program. We just know that no C programs want to have no pointer exceptions, and so once we know that, we can generate this proof, this thing automatically. So the way, the way I think about it is is that if you don't know anything about formal verification, you don't know anything about like, quote, you know serious software development, then you can write a reach program that does something quite useful and some properties will be generated automatically for you and as you learn more, you can take those ideas and put them into practice using the reach compiler. Another thing that I think is appropriate to talk about right here is like the role of audits, like what audits are really doing there before before we run, because that's like that's a whole huge sure, let me just talk about two people talks about audits all times. Yeah, that's like I think we should try to cap that a very little bit. So I'M gonna try to put some of my intuition what you've said. It sounds to me like if you imagine that, you know, you can write javascript program where you can write a type script program and just like that, javascript will do stuff that's useful with zero type information provided intentionally or like implicitly. It sounds to me like the sort of free specification and verification comes from the typing. So you were, as you say, you know, you're like writing the value program, which I guess is the Javascript, and then when you add type script, you are defining the types, which gives you all these like additional rules about what space, like, what what states and and like state space and values can and should be reachable. And so if, from within, that is, if you get your types right, you're getting a fair bit of safety, additional safety guarantees from that. Is that like rough, like good enough? Yeah, that's that's a great analogy because it helps you get that what type systems are doing is they're moving errors that would otherwise take place at run time and moving them to compile time and then, which is why people hate strongly type languages, because the compiler bullies them all day. Exactly well, and there's a good reason for that too. Yeah, not, not not for the bullying, but the hating, which is that you know, we know that Automated Algorithms for reasoning are limited, like the goals incompleteness. Proof is exactly about this, that anytime you have a proof system, there will be theorems that are true that you cannot prove. And so, because of that, that means that any analysis is going to be any analysis that sound is going to be incomplete. They're going to be good programs that it refuses to run. And the goal of program analysis is to make it so that the set of complete...

...programs is as large as possible. You want to try to make the analysis more and more powerful, so the kinds of grounds of people actually want to write are ones that we can automatically reason about. But there will always be a time when you know that a program is right and your compiler will say you're not allowed to run this program if that compiler is backed up by any analysis tool. And that's what I was saying earlier about the way in which reach is limiting because you're programming with a safety net. It's more like you're program with a helicopter parent. You know there are programs that it's just going to not let you do, even though mom I know that it'll be fine. And in situations like that, you know you either need to decide whether or not you want to be purely on the straight and narrow or whether you want to live dangerously and have your reach program interact with a program you know, directly written in solidity or assembly or whatever. Yeah, I think that that was a good summary. Yeah, great, great, and I want to I thought I thought like I also thought your example of, you know, put it really into solidity. I think there's like a kind of a bug, like I liked your example of basically like these these amounts that kind of they all need to add out at the same time, right. So, like there are there are like fairly common there's like a fairly common bug where like you can get token inflation, where the total supply value and token does not increase whatsoever, but somebody can send a token to them so they have five tokens, they can send that token to themselves and they have ten tokens all of a sudden because the the token wasn't doing the accounting properly. So it sounds like you're saying that that's just not going to happen. You know, reach language or I reach implementation. Yeah, that would be an example of a property that would be automatically taken care of because we can, because we know that everybody wants the linearity property, and so, because we know that, we automatically include that. Can I get out of it if I want to? For some reason, you couldn't get out of it exactly, but what you could do is like think of it like this. What is a token? A token is like when you think about in terms of like the data structures, there's a hash table that takes addresses to balances. So That means it's a ledger right to a ledger is this is this mapping, and if I hold those assets, then that means that what I want to do is I want to give you the ability to remove them from the contract. So that means that I'm going to transfer away from me something based on what was in your cell in the Hash table. And so if we, if you wanted to get around this Um and not enforce this linearity, then essentially what you would have to do is you'd have to say that your balance is ten, but you actually can only get access to five of them. So there would you'd have to program and in such a way where you said you're allowed to. I'm going to keep in my database that you have ten, but when it comes time to send them out, then it may fail. So basically, it's sort of like me, as like the reach expert, like I can imagine a way that you could probably do this. It's not going to actually make it so that you can get things that you shouldn't. What it's just going to do is it's going to force the reach compiler to allow you to make a runtime error rather than a compile time error. That's really the way to think about this. It doesn't prevent you necessarily from doing something. It gives you the tool of detecting that that bad thing...

...would happen at compile time and refusing to let you run. So if you meticulously plumbed it, you could make it so that at the very last moment you would see, Aha, I can't do it, and then reach is going to force you to not actually do the transfer, but you can delay up until that point. It's kind of like forcing weird behavior to have a larger domain expertise. If what he's doing, you're she's doing. Yeah, I agree with that. That's pretty cool. You built something to reach. I made it. I made an application. Reach says it does what I think it does. What am I deploying? Because it's not. Because, like I think what's kind of lost in the conversation so far is that it's not just smart contracts, it's all the things in between two, and so that's quite a bit of stuff, depending upon the complexity of what I'm building. Also, hosting infrastructure for where these myriad of things live is is pretty brought depending upon what I'm building. What how does that work? And reach like, where do these things go? Yeah, so I'll talk about what we're doing now and then I'll allude to what we're doing in the future and Christ maybe will comment more and what we're doing in the future. So right now, when you compile your reach program you don't just get a smart contract because, you know, reach is not a smart contract programming language. It's adapt programming language, meaning that when you write your reach program you are saying what the individual endpoints do. And thus, like take something like, you know, swap. You know swap involves liquidity providers and it involves traitors. So the reach program that that is, you know swap, like the you know, an automated market maker. It doesn't say here's the logic for making a pool and here the allowable transitions. Instead, what it does is it says a liquidity provider can come along and they can decide to do a deposit and after they decide to do a deposit, they can decide to do more deposits or decide to do withdrawal. And separately, a trader can come in and when there is something in the pool, they can they can send in a trade and then they can make that trade. And so from these descriptions of what the individual participants do. We can derive what the smart contract is, but we also have the specification about what a trader is and what a liquidity provider is. So when you compile your reach program you get a middleware layer, a back end that drives a particular liquidity provider using this contract, and you also get another program for particular trader. Now these programs use the reach SDK, which abstracts away the details of the underlying networks. So, if you know, it basically allows you to have like a uniform way of programming using, I'll grand and etherium and, you know, future chains that will support. And then you can take that middleware program and you can write a front end for it. So you could write a user interface, you know, using react or any other job script library. You could write a front end in another language like python and go, because we have a way of allowing you to write those front ends not in Javascript, or you could write an automated front end that was like a test suite, basically that like automatically drove your application. And if you go, you know, use the doc look at the documentation. Basically, the first big part of it is about writing an automated one and then we say, Oh, here's you could write a command line, you know user interface, and then here's are you can make a webbinter interface. But now suppose that you did that and like now you want to quote launch. Like what do you do after that? Well, what you could do is you could take your webb interface and, you know, put it in an sthree bucket and then people can go to a website and then now you've launched your application, because your application in beds, inside of it interacting with the smart contract, deploying it, launching it,...

...and people can go to your so you can make it so that your application, your web application, drives the entire process. Similarly, if you wanted, you could take your you could you could take your your back end and embed it inside of an Ios APP and then you could build a front end inside of your IOS APP that contacts that and drive the creation and interaction with the smart contract directly from the APP. No one's actually done this, by the way, with the IOS up yet, but in principle it's possible to do that. So anyways. So that's what you get when you compile your reach program and reach does not mandate any particular deployment strategy. We provide you with those tools. I think the main thing that that that reach does in this regard right now that's, you know, Nice and automated, is that it provides a doctrized infrastructure for you to run your automated test programs. So basically, when you write a reach program, you know, you compile it and get these artifacts, but you can also use our command line tool to or o vs code extension to run your reach program and what that does is it will launch a custom Dev neat for whatever change you want to test on and it will run your test program against them so you can make sure that they work correctly in the long run. One of the things that we would like to do is provide a, you know, a Hiroku style service where we can help people launch their applications. But if we want to talk more about that, I think that you know, Christ can comment on that. Business Guy. Yeah, the there is there's a lot of ways that we were actually going to be monetizing this in the actual future, but right now our main focus is all about traction and getting this in the hands of many, many developers. I mean, and I it would be a long podcast all by itself, of the ways that we're going to actually monetize. But so, yeah, all right, great, that's a that helps clear up a lot of the money. Just that I currently felt about kind of cool. I wrote something. Now what do I do, because I have to deal with infrastructure a lot and how these things interact and so on and so forth. For those who are interested, what you've mentioned it a few times, but explicitly. What, like back ends are you supporting and what's on the on the horizon for future backends that people can deploy sough. So currently we support the EVM, so anything so etherium, and then any chain that's has a IBM back end, and then Algorians are both fully supported. We are. We've recently partnered with conflux to help our strategic partnership, to help us actually grow into China, because they put a lot of time and effort over there. So we have recently partner with them. But in the at the end of the day, our goals to be able to be integrate with every major chain. This is not something that's only picking like the top two or three. It's just that at this point we believe that between etherium 'l grant and conflux will be able to actually hit our goal of Sixteenzero developers in the next eighteen months. So no need to actually add new chains until we actually deepen the amount of features that reach a self provides, and at that point we'll start opening up to other chains again. John, guys are and I didn't really the audit thing is hanging there. I think I'll just like, I'm curious what the comment is. I don't think we should really get into like an open ended conversation about it, but you know, give you opportunity to feed. Sure. Yeah, so there are really great audits out there and there are poor audits out there, and many audits have the form of I am really smart, I looked at this program here are my...

...comments about it. Sometimes an audit will say I use these automated tools and I in an I reasoned about the output and here's my advice about what to do about them. And an audit like that is something that is providing interpretation of automated tools that the authors of the program might not be able to do. And many of the automated tools that people currently use when they're analyzing and auditing smart contracts would not be necessary for reach programs because those checks are built in to reach itself. Now, another aspect of auditing that's very valuable is when the auditor says, your program is supposed to be a program like this and programs like that. Should really check this unique property of that particular thing. So, for example, you know you might have the token linearity property. Or if we were to think about traditional softwa development, maybe like if I am, quote, auditing a sorting routine, I'll be like, well, you know, sorting routines really should produce per mutations of their input, and I noticed that your program didn't have an assertion that the output was a permutation of the input. And so what an audit can do is they can provide additional assertions that the programmer should have included. Now, when you're programming in an environment that doesn't already have the ability to do verification of its own, one of the things that happens is is that the auditor will say, I thought of this assertion and I reasoned about whether it was right, and maybe I reasoned about whether it was right using automated tools or using the custom verification environment that that I deploy in my audits. Now, if someone were to auditor reach program what they would be able to do is they would be able to say, you really should have put an assertion here online seventeen, or over here on line twenty, you should have put an assertion there. And basically what this means is that the reach compiler itself is an automated formal verification tool that auditors could use to be the facility to check the assertions that they come up with. So I think that there is a role for those kinds of high quality audits where someone would come up with the appropriate assertions that would increase confidence and the correctness of a program and I think that the same way that we currently look at smart contract developers and we say that it's good for them to do audits. Doing an audit doesn't mean you're a bad smart contract developer. It just means that you are responsible and you're trying to go above and beyond what some people do, and so I think that it is totally appropriate, with that mindset, for high value reach programs to go through audits of the same form, except that those audits would be in some ways easier to do, because the reach compiler itself would be the verification tool that would be used to deck the program and the Nice thing is that those assertions would then live inside of the reach program in the future as the program would be modified, so that the program would need to be continually audited over and over and over again. I want to add to that a little bit based on what I've experienced using it and listening to you talk and like kind of the development process of writing a reach program. You're kind of pushing the user to do a lot of things that we, as security engineers or people who do audits or have been experienced with thoughts, try and get developers to do before they even start programming. That's things like threat modeling, user stories think like and and risk analysis and how these things interact, like how users access risk and whether or not that's a reasonable thing. And because you're programmatically talking about users in the process of writing a reach program, they're kind of doing that. And so, like we'd like say, for instance, someone would...

...a reach program, they're able to extract and a lot of ways, what the programmer thinks about all of the possible individuals that could interact with this program, how they interact, how they reach, how they access certain types of risk, and the compiler make sure that what they've encoded does that and then, like, as an auditor, I can take a looking like well, this is going to end up in a scenario that you may not a thought of. You put in a social searching here to make sure that doesn't happen. I think that's what you just said right. So, like, like, because you're thinking about in a process of quding the individuals who were doing things and how they interacted each other, you're actually codifying the communication and interaction between individuals and then extrapolating a lot of verification based on making sure that communication is proper or like, if is done well by the code, you're getting a lot of the things auditors want developers to do or like a lot of things that like the concept of a secure development life cycle it has, and a lot of the things that no one's actually doing. I agree. I'll this all this ICH that I think like, yeah, having it the the real thing I like is having in the code, like not separating the specification from the code, because I mean, like even just comments, like I generally prefer not to have to go do like Doc's diet, your protocol dot i. Oh, I really just like want lots of comments in the code. So I'm but then you know even better if it's it's code in the code that describes the code. And Yeah, secarating that does something, much does some. So I very much agree and I feel like, you know, when other in similar environments, people would say, Oh, you know, you should do these things in your driva program you should do these things in your c program but there's very little payoff for doing that. So it's like telling people to take their vitamins or, you know, exercise or something like. We all know it's a good idea, but you know, it's very hard to do it. And one of the Nice things is that, because reach also generates that back end layer, the reason that we generate the back end layer, or rather the only reason we can generate the back end layer, is because we have this information about the individual participants. So by actually doing something more for the user, we make it so that they produce those residual artifacts that are useful for the security verification. So like, I feel like when I think about reach, there are all these little components that if you just focused on one of them, you know it's no, it's kind of interesting. But I think the thing that makes it quite special is the way that they all kind of melt together. Like we have this high level programming language that has a new model of blocked of adapt development. It's design for something that total beginners can use and it's and it's paired with this, you know, Verification Language and verification engine. That's a very full featured and all of those things work together to produce this, you know, harmonious synthesis. Awesome, Chris. What's next? What's on the horizon? How do people figure out learn more, get involved, try it out? Like give you an estimate. I'm like how long it would take? Somebody you are did this for your previous employee, but like chill yourself to our audience. In a sense that like if you started using reach now, you could deploy at application and x amount of weeks. One Week is where we were. It kind of sad that it takes about two to eight hours to get through our tutorial, depending on how deep you want to go down the rabbit hole of the everything that we do, and a lot of people don't like to sit and just do that Allan one day. So I like to say, you know, spread that over a week and by the end of the week. Our tutorial actually launches a formerly verified wager based smart contrary Depp that...

...can launch on multiple different chains and it's very easy. You can get to get to our documentation at dock stout, reached out sh as far as what is next, Jay is and team is actually working very hard on rolling out more and more features so that we can build out and compile more different types of applications. But, like I said earlier, our goal and are actually, it's showing, pretty realistic at this point. That's, in the next eighteen months will have sixteen thousand developers that actually go through through the actual reach tutorial and start building applications. All right, trying to get anything else. All Right, thanks to come on show, and that's the luck guys. I mean, I'll be looking further and further into it because I like the concept of lowering the barriventry for secure development and this seems to be it. Excellent. Thank you very much for having us. Thank you both.

In-Stream Audio Search

NEW

Search across all episodes within this podcast

Episodes (127)