Oh, I don't think that coming up. Yeah. Do you want to do like an AV test share screen or something? Yeah. Let me see. Can you see my thing? I can. Yes, I can. Zoom is like, I think that way fairly reliable. I had a lot of friction yesterday with Google Meet.  Social media, whatever it is. Yeah. And then, then we can do it again. Like, you know, I think it's better with that way. I don't want to waste your efforts. No, it's okay. Like we can just like, but you are not available to do it also. So yeah, we can just report.  And the fact that obviously they can efforts, they mean a lot. I was just posted it on our internal Slack. I think one of the folks from my team are definitely interested. Shalott joins one though. That's how I got reminded Hey, hey, shalott. Hi. And let's go. Eventually maybe another five minutes and then then let's let's start. What, I think let's get started. Yeah. So, like, so we have a lot of, let me do like a quick, yeah, just to quickly. So like, hey, everyone, welcome to PWL Bangalore. As you know, by now we are reading developing verified programs with Daphne. And Devanshu is going to go through the paper present his findings. It's a small paper. I think we'll probably done in a short time. There are two papers with Daphne. One is the Introducing Daphne Paper by Microsoft goes into depth about the language. And then this one, which is an easier introduction where you just go through a bunch of examples. The idea is that you develop a verified program using Daphne. It has a, other than being a general purpose language, it runs static verification. And fundamentally addresses the question that, hey, whatever program you're writing, is it going to work as you expect, right? Which is actually, if you think about it, it's a pretty difficult problem to solve without some kind of static tooling, right? Tests and higher kind of types only do so much. Yeah, the whole angle of static verification, meta languages, et cetera. There's a lot of programming languages research behind that. Daphne is just sort of like an introduction to that. And I'll let Devanshu go in depth on that. But yeah, I think let's get started over to you, Devanshu. Yeah.  Like, what do you do? Maybe like, you know. Yeah, so yeah, hello everyone. I'm Devanshu Dhanjan. I've been working on experimenting with like, functional language and proof variation for like, for a long time, maybe two, three years. And, but I work at Google and I can't be at work.  It's just a side thing I do. So I've been experimenting with Daphne for like quite a few times. Like, I have tried to experiment with Daphne for quite a few times. But for last one year, I have really started liking the language and trying to prove few things with Daphne. Before that, I have also experimented with Kov and Arda. And so those are also like very fixed in language for. So, okay. So this paper we were talking about is developing verified programs. It is written by Christian, you know, who also developed the Daphne and yeah. So I choose this paper because this paper is very easy in the sense that it's kind of introduction to programming in Daphne without, but it is in paper form. So that's why I chose it. So before going and deep dive into the paper itself, like I will say something about verification or theorem proving. Like, even though you are not like proving things in your day job, but like these kind of concepts are very helpful for software developer. For example, reasoning about programs is like it's the one of the first time in the paper is that reasoning about programs is a fundamental skill which every software developer needs. And this is needed because sometimes you come across certain kind of bugs and whenever you are debugging that bug, you kind of reason about program, but you're not doing formally, you are doing paper or pen or you are doing mentally. So you are doing reasoning about programs and second thing, reading all these things is helpful because this gives you a list of words or vocabulary so that you can communicate your idea. For example, like if you read about literature, you know what invariant means, what precondition means, what postcondition means and those kind of things. So even though you don't use in a day job, it's helpful skill to have. And yeah, and okay, so now we will know this verification or reasoning about programs in Daphne. And Daphne is like mostly imperative language, but it also have constructs for like a functional and also object related. So and like good thing about Daphne is that like the value to enter for like to Daphne is less than other proof assistant kind of thing. For example, all the above. So it's very easy to pick up with Daphne. If you don't have any experience with like, if you don't want to read about theories and stuff like that and you just want to play around and you want to prove your imperative or objective in the program. So that's why it is very easy to pick up. And like one more thing is that which I did not mention is that Daphne is also type language. So you have to explain like this construct is type and also besides these functional objected and imperative, it also since Daphne is a verifier, you can have construct like this method needs some preconditions and that and this method returns some post like maintenance that post condition. So whatever behavior you want program to have, you can specify it. So like since this language, this paper is almost like an introduction to programming. I will just jump into the editor and we show you the first program, which is paper mentions. So let's jump straight into the editor. So first program, the paper mention is that you want to have a method which source three integers. And just like every other language, Daphne has a concept called like method where you want to declare a function. And since Daphne is a type language you have to provide every input and output parameters as a type. So let's say it takes a three parameter as a three integer as an input and also returns three integer as an output. And what we want to do here is that this construct is like you can find in every language. For example, this is a normal method which takes three integer and returns three integer. And what we want to do is that we want to return A, B, C, but we want it to return in sorted order. And in Daphne, as you can see method return type R name. So like for example, like there are three returns, three integer which are written and both like three integers are named for example, they are named X, Y, Z, Y. So what we want to do is that we wanted to return A, B, C, but we want it to be like sorted. So like what, so first thing we do is that we just assign these integers to A, B, C and then we do some comparison and try to return those values which is signed to them. So like one thing you can do is that you can check that whether Y is greater than Z or not. So you can just, if that's the case then you can just swap those values, right? And you can do the same thing for X and Y also. And maybe you think that this is right. You think that this will return sorted A, B, C in sorted order in X, Y, Z parameter. And since Daphne is verified and it has other constructs which you can provide that your specification it says that whatever your input is, the output is sorted out of that input. So you can just, so in Daphne the way you say that that this is the first condition of the method that method returns that works like maintains that first condition is using ensures which you provide after returns. And here I wanted to say that X is like, this is the sort of which I want to provide. But now you can see that Daphne is complaining that it can verify that whatever I have method in my mind is not correct because it is saying that even though X is less than Y Y is not less than Z. And so it's saying that like your implementation is wrong in the sense that one of the post condition is not maintained. So we can ask Daphne what it knows about our method at this point. So it does knows about that X is less than Z and like X is less than Y. But like if I ask Daphne does it know what Y is less than Z, I think it's heading out. So like if you think about it, you understand that we are one comparison sort. So you need one more comparison to swap Y and Z because after swapping between X and Y, Y can also be less than Z. So we need one more check and then we can just a second. And then we say swap the thing. Now it is saying that your implementation is correct. It is saying that you are returning X, Y, Z but and the X is less than Y and Y is less than Z, that's what we wanted. But there's one problem with this thing is that I can just say that X, Y, Z is this and I can just delete these things. And this also verifies because our post condition is right and there's nothing in our specification which says that whatever I am returning is permutations of the whatever I am getting. So our post condition is not strong enough. So we make that our post condition is more strong that our input set is same as X our output set. So this is how working with Daphne looks like and this is how you define matter and like how the syntax of graph look like. And in the beginning I mentioned that Daphne has concept of like return type has name that you can see why the return type are named because you need to refer to those names when you are giving the post conditions. And one more thing I want to mention here is that the don't explicitly run in Daphne like when conditions goes to the end of the statement like method statement it just whatever the values are there in the output parameter it is done. If you want to return you can just write return X by X but that's what you find but in Daphne generally people don't return they just don't write specific return they just assign to value what the return parameter is and then when the control which is the end of the method it just returns. So this is the general favor of like how the meta definitions and how we can do like small like function verification in Daphne if like there's questions like I think I can take questions right now. So perhaps we can look at like a slightly more complex example or something. Yeah, so I will go through the examples like example like later but like let me go back to the paper and see like something the paper like something which is mentioned in the paper is something which I missed or not. So yeah, so like so Daphne like goes through all the parts or like there are multiple branches in this method and Daphne goes through all the branches and see that whether in all those branches the post-condition is verified or not. So and as you can see the Daphne verify runs in background and it gives you like a nice feedback loop like these things are right and these things are wrong. And yeah, and insurance is how you can write up like a post-condition to the method. And like before going like driving into the harder into like further into paper I also want to spend a like a small more example so that you can have a little bit idea about how Daphne works internally. Let's say you are writing a method let's say call it A and let's say so in Daphne so this in source is how you write up post-condition to your method like for example what is the conditions between the return parameter and input parameter which holds after methods returns and requires is how you say that this function is allowed to call only when these conditions holds for example I can say that you are allowed to only call this method when A is better than 10. So this is how you do it in Daphne and since I want so want to return something let's call this returns and I want you to return our integer which is named B here and let's say I assign two times A. Okay, just like I said Okay, and now I wanted to ensure that B is also better than 10, right? So this verifies but like I'm giving this example because I wanted to show like how Daphne works internally and like what is the like give you a small idea of like how Daphne works internally So let's say here Daphne needs to verify that D is less than 10, right? And since this is a internal like this is the like assignment expression we can just swap D with A and here Daphne need to verify that two times A is better than 10. The process of like taking verifications like going to the end of method and going step by step to the three conditions and calculating this Boolean expressions which need to verify this is something called the case three conditions like the process like this is so here I wanted to say that B is less than very less than 10 and for this I have to prove that before this assignment two times A was better than 10. So here I'm converting some pre-condition like some conditions to some pre-conditions and this pre-condition I'm asking is with case in the sense that it like income passes more program state for example if A is 20 here also then our program verifies but A is equal to 20 kind of like smallest our program state so that it's not the case pre-conditions but two into A greater than 20 is kind of the case pre-condition in the sense that we're asking like smallest constraint on the program state so that our program kind of verifies. And then we are given that A is greater than 10 and then we have to prove that two times A is so this is something Daphne tried to prove and the way Daphne tries to prove is that since this kind of like formulas are kind of first order logic and it converts this logical formulas to check three formulas and it offends that formula to check three solvers and like if check three solvers says that this is true in general then Daphne verifies this program so this is the general idea like how so this is like I give a statement like give example when the only statement it has is assignment so these kind of like taking a condition and like what condition before that instance should be so that our condition verifies is called because the conditions and it does for all kind of statements like for if, for why you for all these kind of things it base those three conditions up to it hits the start of the matter and then when it hits the start of methods it has some kind of a start of method has some kind of three conditions and it verifies that after taking those three conditions into hand those conditions which we arrived at the beginning of method is very good not so I can take any further questions here if something is not clear or stuff like that if anybody has questions like just drop them in the chat I'll summarize and ask at the venture or feel free to like unmute and speak up yourself we are pretty small crowd today so unmuting and speaking should be okay if not I think the venture let's continue yeah okay so this is the general like generally in program we write method and we want to verify these methods and we saw that the question is how you do it in the general in method but since Daphne is written for like imperative kind of programming in mind it needs to verify the loops also and for verifying the loop there are various ways in which various tools and various verified tools does these things one way is that somebody if I does like loop unrolling for example they will like try to see that what if loops run zero times and if loops run zero time things verify one all what if loops one times and they do unrolling up to fixed number of times and see that runs verify or not this is one way of doing it and like but Daphne uses a different way to like verify loops and in Daphne you have to provide something called loop invariant to prove loops and in the first case you don't have to like in loop rolling unrolling you don't have to prove like provide an invariant because after you unroll the loop it will be either a statement or if a statement or stuff like that and the verify knows how to calculate the case preconditions from those things and doesn't need any extra help but in Daphne case you Daphne needs and help in the sense that Daphne need you to like provide some like summary of the loop so that something which doesn't change in the loop and so that it can verify I think it's better I switch back to my editor and show you like how things work in Daphne and give you example and give you like running example and give you like a live demo of like how it does in like how it looks like in Daphne so I'm picking only those examples which is mentioned in the paper but like if people want I can also give like other examples Hey Dupanshu, if you take a few minutes for here there's a question on YouTube I think is the which is useful for the whole audience is that what kind of problems are we trying to solve with the Daphne? I think what the asker is trying to get to is like what is verification ring and what are some use cases where is it used, et cetera you wanna spend before we dive into an actual program? Yeah All right Yeah If you managed to talk about that Yeah, so okay Let me bring this Okay So like for example, let's say this program like there are various ways you can say that you have, when you write some program you have some specification in your mind like for example, this program does something like you write program for doing something and how you verify that the program does what you intended it to do one way is that you can write test and test is like easiest way to do that and but like if your method you are right it's very complicated and it has lots of branching and stuff like that you have to write lots of tests and you also not so like like you cover all things in your test or not, right? So like what brings is that it kind of gives you a tool so that you can, it gives you a language so that you can write in a programming language what your specification is they generally like people write in like other language they will write in comment like this program does that or maybe like in some language then they are on separate passwords so you can just say that at this point of program this thing should hold otherwise I will just pay it off but that's done in the runtime in most cases and but yeah so like one thing it gives you that it gives you a language to write your specification and other thing is that it also tests like your specification holds for all the parts like testing is one way to do it and specification is another way to do it so yeah, if I don't know whether that answers the questions Yeah, I think it does and to add on to that like honestly there are many ways of verifying the correctness of a program and the most popular way is writing tests but it's often not enough and the idea is that there are more advanced and far better mathematically proven ways of doing things and this style of writing program is one of those disciplines and so if you think about it from that perspective the applications are as such limitless there is no specific use case built for Daphne that okay only write this kind of programs anything like as long as in the language paradigm everything allows can be used for Can I ask something if you guys can hear me Yes, we can hear you now This is the laver I write kernel drivers once in a while Windows kernel drivers and Microsoft gives you a verifier which runs in the background and make sure that your driver is not doing something silly with the memory right and once in a while I would like to use these kind of tricks inside the C program or C++ program which we are writing right so that part that you know your verification is also part of the program is very enticing and definitely because the previous couple of things I try to look at now behind the digital diagrams I think BDD based other LTT something which I don't understand it very well but they were all like you have to write a wrapper around the program or try to describe the properties you want to solve first so I have two questions here is that from the development perspective can you disable the verifier once you are confident okay fine my program works fine so your binary which goes out in the production does not have that verification layer so probably it works faster efficient consume less memory and second is if we just look at the existing these tools or where these very verification for instance one of the language I forgot its name is very popular by this very famous computer scientist if I recall the name I'll say it he also has this language for formal verification I mean if you compare in contrast is it as powerful as any other or is there some disorientation or advantage probably that will also help people who are using such tools okay yeah so so for answering the first questions whether this asserts or ensures run on the like like these tests are run on the runtime no so these tests are a static verification so like whenever like Daphne is generally using Daphne you can use this out porting like few languages python is one java and koi is also supported so when Daphne spreads out like if you write a program in Daphne and you want to spit out program in those languages Daphne removes all these asserts or post conditions and preconditions Daphne verifies these things statically so that's one thing and every for instance again persons every form variation tool has some kind of limits and like some things might easy to do in some language some things are hard to do in some language for Daphne like like in general I think I picked up Daphne because it's very easy to demo for software engineers but like in general like you can do like everything in Daphne which others goes to for example like like as far as you know the one of the earliest formal recognitions of the pixels was done in Daphne from like by iron cloud people from Microsoft so yeah I think yeah if I don't know whether that's you have further questions or you want to expand on yeah I'm not sure how much time I can take but I have one additional point actually just to probably highlight the issue which I'm trying to get so as an electrical engineer you are once once in a while you are interested in those liveliness properties of the state machine that eventually this will happen or it never happens or it happens after a certain number of steps right so what I'm not getting at looking at this method that the time how the time is encoded that this is all of this is true when the function is called or this also keeps track of that eventually sometimes this is violated and the only time you get that how shall I say the proof of the violation or it's something theorem proving kind of thing that without running the program I can say something like eventually this will happen or it will never happen so on and so forth yeah so like this don't have concept of time in the sense that it takes parameters and it spits out the parameter but to answer your questions if you wanted to prove liveliness property with Daphne it's possible I will point to your paper like this paper is called modeling concurrency in Daphne it is written by Christian you know and it gives you example like how you want to encode liveliness property in Daphne so it's very nice paper if you want to prove like liveliness property in Daphne you can do it that is hard to thank you yeah so okay if there is no more question I can just give an example of like how loop environment like loop like how we verify loops in Daphne so this is like we will write a small function which calculates the triangle number triangle number is like like four and it is sum of number up to n for example one is one two up to three like for two it will be three and for three it will be six kind of thing so like there is a close formula for that triangle number and you can also write a loop which just sums the number so let's just and then we will add variation and see how Daphne reacts and what information Daphne gives so let's write a triangle number I want to write and then let's assign it to zero and then let's have a loop variable which will go to n and what I want to do inside loop is that I do this and then do this thing okay this looks right like since there is no like no verification in this method Daphne is just is fine here but like even though there is no loop Daphne does checks that your loop is not infinite loop for example if you do this it will complain that Daphne cannot check like Daphne cannot verify that whatever loop you write is not like it will finish so like without without any specification Daphne checks one thing that your loop page kind of like like there are fixed number of iterations your loop does so this is one thing I want to mention and then let's write some conditions one first condition I want to write is that whatever I'm calculating like since this is a triangle number we we know that it has some fixed like first formula okay so like if you write this thing it's like Daphne doesn't complain that it cannot verify because just the paper mentions for to reason about a loop in Daphne you have to write a loop invariant and the way you do is that you write invariant and then okay so let me tell something about invariant invariant is something like you want to like invariant is something even though you write loop for you write loop to change something like you assign to some variables or like loop index is always changing but like even though in loop things are changing there is something which are kind of unchanged in every loop iteration and those properties kind of specify what loop does and here one one thing to mention is that even though i is changing the current value of t is is triangle number up to i so we can apply that so let's write that like even though you write Daphne is not able to verify it let's see okay yeah even though because let's ask Daphne what it what it knows about this point so one thing you can you can you can add additional assert so one thing Daphne knows that that loop's finished so it knows that i is certainly greater than equal to n right right and i think it also knows whatever value of i is it is equal to b what it doesn't know is that i is exactly equal to n so you have to also like for example since you can also like if not like you can also implement by two so like like it is not always the case that whatever the loop conditions you provide the variable will always like after the end of the loop will be the same as the as the whatever the conditions you have provided for example if your n is like five and you're starting with zero and you're implementing by two then like after end of loop i will be six so those kind of things because of those kind of reasoning it doesn't say that after end of the loop Daphne was that i is equal to and it knows that i is greater than equal to n but it doesn't know that that it is equal to or like equal to n so you have to provide one more invariant to Daphne that whatever the value of i is it is between zero to n okay what did i miss okay now it's saying that again this environment doesn't hold because like invariants should also hold when the when the first time it enters into a loop and what happens if i call this method with a variable number in that case i am assigning i to zero and then at the start of the loop it's not possible that i is greater than some minus 10 so you have to add some pre-condition to this method like i want to um i want to provide some uh just a second i forgot how to provide yeah the quads i forgot the keyword for providing the environment so i have to state that whatever i'm doing like this this method will always call when n is greater than zero now Daphne verifies everything and and this is how experience of a refining loop in Daphne looks like so when providing the loop any invariant like you have to think about like what i wanted to prove our program after writing the loop and whatever the invariant i am providing was sufficient enough to prove those things so this is how i think about like when i'm writing a loop invariant in Daphne um there might be other way to think about it but i think um yeah that's that's how i do it like um like what i want to prove our after loop ends and how how strong loop invariant i should write so that it can prove that thing so if any questions about how like uh loop invariants are like other things still now i'm happy to take any questions right now yeah so i think uh sudar is asking that it should not be able to prove whether the loop exists it's not it's technically not the same as holding problem but uh because uh loops are are deterministic but i'll i'll let Devanshu address that yeah so uh in Daphne you in Daphne loops you cannot do all kind of computation like like like you can like you can uh if you write some kind of program which kind of imports holding problem Daphne will complain it and there's no way for you to prove it because because this is the like uh like because of holding uh theorem so yeah there there because it's uh you like uh you cannot prove it you might write it in Daphne but you cannot prove it that it will uh so you have to you have to uh what you have to do is that like if you wanted to write those groups where you say that um i don't know whether this loop by default Daphne uh assumes that whatever you're writing is finite computation but if you wanted to do something like you don't care about like loop exists or not whatever like you provide the pages and say a star like i don't care about like this loop exists or not so yeah that is one way to do it but uh shouldn't shouldn't we add the so let's say if we are uh changing variable value within the blue uh uh is it necessary i mean uh will it automatically figure out that we are changing the variables value or should we uh definitely add that to the invariant plus to the top uh yeah so yeah so yeah uh yeah so for proven termination it doesn't need invariant so uh so it is able to prove that uh that this product exists like like this loop like finishes but like i need this invariant to prove this statement like uh that uh that after loop exists uh then i need uh this loop invariant to prove these things because using this and this i can say that after loop finishes i is exactly equal to that but loop invariant is more prepared for prove termination in this case okay let's go back to paper and see if i miss some points uh which i wanted to mention uh yeah yeah so uh like uh the way to think about this uh loops is that when verifier checks uh region about the loop it doesn't after loop finishes it doesn't look into the loop only it only reasons about loop whatever uh based on what invariance is provided so uh so you have to very careful about what property you want to use after loop finishes so you are like provided as a part of invariant okay uh so next thing i want to mention is that since daphnie has all these uh like different way to write programs it also has like uh price or mathematical functions so like you can write fewer functions with daphnie and uh there's there's some virtual intervals like uh like how you write functions with daphnie and in general where we are writing statements uh when you're writing uh methods but when you write functions you have to write an expressions and syntax of functions are a little different than method and functions are given so since functions are expressions you can use them as a part of like your verification conditions you can you can call functions in your insores and request clause you can call functions on on your invariant clause uh uh so so yeah so before going further let's give the like let's go to the example which uh which the paper provides and uh let me give you a test a test of how it looks like in daphnie so this is uh yes let's say you want to write a function which calculates power of two and just like a method uh if like you provide a input time parameter and the input type but the since it is an expression and in in the function you can only run one kind of like you cannot return multiple uh output expressions so you you provide whatever the output type is with uh sand colon and colon and with uh and in method body you provide your expression it's expression not a statement uh it's a tricky thing I also like like do that mistake sometimes uh I write a statement in the function instead of like writing expression so let's write what looks it looks like here okay uh so this is how it looks like and daphnie high quality comes in that this this uh this is uh it is it is not able to turn it so you have to provide like uh uh request clause that uh you're calling the flip sign as well as zero uh so that now so this is how you write uh notice that I haven't uh committed to this uh statement like statement the same column so it says expression so that's the only point I want to mention and uh uh so this is like uh we will see like how how we can use functions in daphnie uh okay let me give you an example like how to uh use this uh function in verification and uh like how it is later in the later in the paper but let's do let's dive right into it so this this is the kind of in the power of two uh uh and uh there is like a efficient way to calculate power of two like one is uh called successive square where uh for for like currently the complexity of this method is n but uh uh but successive squaring does the computation in log n so so you want to implement that method and you want to do so that uh whatever this is calculating is the same as uh um the successive aspiring computing so let's just write this uh uh long uh complete power and just like uh our function it also requires that n is greater than zero and since it's a function I have to write what I'm trying to do down here and we will add the post condition and specification later after we write like uh simple logic so this is how you can success successively uh like uh square things and calculate in log n square so if n is equal to zero you can just say that uh uh then what do you want to do is that you can just say that compute power uh n by two and like you you want to multiply uh two runs so that uh it is squared else right uh so this is like uh way to do it like uh uh successive aspiring it's calculating in log n square you can see that it is log n for example it's half half in the and in every call and uh since we are using duffin you can uh say that in source uh let's say whatever the easy training is power of n now uh duffin complains about it because um it's very tricky to prove like uh it's very tricky to prove uh you have to provide some help put off me to prove it and uh let's go go through it so so for example here you can say that you can tell that uh things like asserts power two zero t is equal to eight one so and since uh p is equal to one both are equal and this condition holds so the average is not complaining about this doesn't verify in this uh branch it doesn't also uh uh also uh like uh you're out in this branch also because it knows that uh t is equal to power two n minus one and uh and your p is equal to two times t and you are calculating one up so you're you're multiplying by two here it's tricky in the sense that for proving things like this you need some kind of induction so that uh uh induction and some kind of uh just you actually need some kind of induction so that uh uh duffin knows about those things so one way to do these things in duffin is try the uh lemma for example you want to prove things like for example when uh when n is equal to like for example uh here duffin is duffin knows that uh for example duffin knows that assert is equal to power what he doesn't know is that uh uh like for example power two n by two into power two is equal to power two n so these things doesn't know and but it knows these things so uh so you have to prove these things explicitly and uh after you prove these things you can just uh use those uh lemma or methods here I will show you how to do it uh so so so so that you are you guys are clear like where duffin is not able to figure out and where these things duffin knows so one thing we wanted to uh have is that we like okay so let me talk about something called lemma like I have I have started talking about these talks earlier this is mentioned in the paper in the hand I think it's uh since I'm talking about functions and compute power and lemma are mentioned in the in the hand and they use this uh function definitions so I think it's easy to do it in a single go so let's so lemma is something which is uh which is kind of method but here everything is kind of a specification you don't like uh you don't write a code which will run it's just used for verification and by verification I mean like you wanted to prove something which will be later used for proving like this this method so what do you want to prove here with that what we want to prove here is that let's I'm using okay let's use this thing and since lemma is kind of method it it it has all those things uh like you can have require and installs kind of thing so let's write this this is like where and what we want to show is that in lemma is that okay and we only want to prove these things for when and we only want to prove this lemma when and is it even number and what we want to prove is that when any is given number uh this holds true right and like okay let me see where this uh Daphne is airing out okay saying that I have used the same name okay now uh this lemma I have written but Daphne is still not able to verify it because uh it is the same it is facing the same problem which uh it was facing here but like when you write proof in Daphne you write this lemma and see if this lemma helps or not even though you haven't proved this lemma let's call this lemma here and see that if our original methods verify one time so let's see that if using this lemma solves our original problem and it does so I think this is the right lemma to prove and we'll prove it uh so uh like one way to do is that like check uh like for n is equal to zero Daphne is able to prove or not it is able to prove uh only the like when n is greater than zero it is not able to prove so what we can say that since it is kind of like you wanted to induction here you can just say that um like you can call induction hypothesis here like for example like prove these things for n minus 2 and Daphne very like so I will go into more detail like why this is happening and Daphne is doing lots of things in the in the background which I will just explain and uh and why it is able to prove it so let's say um so here it is you can you can see that it is able to prove because uh power two zero is one and power uh like uh like zero divided by two is zero so it it is able to prove but here what we wanted to prove is that uh assert power two n by two power two n by two so uh so here what we're saying that call this lemma for n minus two so here and Daphne knows that uh let's write this down Daphne knows that now after calling this lemma Daphne knows that power two n minus two divided by two so since I am calling this recursively Daphne now knows that this is true and Daphne now has to prove that and Daphne what Daphne does is that uh it does power n is equal to two into two into power n minus two and then it okay I have missed these things and what it does is that uh it splits out uh like this equals sign and then uh multiplies two to each part and then like add the exponent and see that it is equal to n by two so this is how uh like internet Daphne does it you can write these things specifically if you want to and there's a there's a there's a way to do it in Daphne in a right in a nice way I'm going to be writing all asserts there's a concept called policy which is like you want to do calculation this kind of good calculation and it will be very easy to look into but like Daphne like when you're writing the proof it's like it's nice to do in this way but like once you know how Daphne like does internally you can just remove these things and uh you can write minimum amount of information Daphne leaves so yeah so this is how now you can see that uh like here I have used the uh our functions in our specification so since functions are a statement and you can use a statement with any source and so yeah I will pause here for some questions and any comments checking on YouTube really quick okay at the moment no questions so if we deal with the floating point numbers how much of this is still there oh so like depends on like how like uh since Daphne uh offloads this carriage to jet three or assembly store solver so like uh like um how much floating point uh theory those jet three drives is what is supported by Daphne okay well I don't know anything about the the underlying engine so yeah I can I can yeah so so yeah so like I give you like a short answer like for example since this uh uh like in the earlier talk I'll talk about which is preconditions and those preconditions are um those preconditions are boolean logic and first order logic and those first order logics are you can solve using SMT solvers which are very efficient in solving those kind of um um problems and then on the top of those they provide some kind of theories for example they they know that um uh like uh addition is uh like like order of addition doesn't matter when you add in two numbers and those kind of theories they provide additional structure on the top of that and uh yeah so like they have inbuilt theories for floating point and um they might not support all the like mathematical theories which floating point provides but they have uh some uh in and also across uh structure and whatever they support Daphne will support it so I'm guessing if you can construct a boolean function uh then or it took table then then it's okay otherwise you are not in luck is that right uh like boolean is not important here boolean is an instance that like uh like for example um like boolean is not important in the sense that it is like whatever you can uh inquiry in first order order logic should be uh like uh you know if you can support Daphne can support and Jax you can support I think so Anand shares the GitHub Apple so I think I need to read up a bit thanks yeah yeah I mean just to expand on that D3 it's an independent theorem broker from Microsoft you can look into that it has other other layers is it integrated with the Daphne yeah yeah so so like uh so like let me give you like a small overview like how Daphne was so Daphne uh takes this uh this syntax and converts to a intermediate language which is called boogie and then uh boogie converts those uh statements into the directory and I think I can show you right now so like here Daphne is converting these things into the boogie so this is the intermediate language like it has lots of uh all other Daphne questions and then you can convert these things into Jaxi and yeah let me see that yeah it is a big file so so this is the like um Jaxi file which uh uh generated by boogie so but like it's very not fun to look into because it has all the internal structure of Daphne inside it and it's very hard to figure out uh where are the dependencies so yeah so this is the like um like um what the Daphne uh sandwiched to the Jaxi so yeah any I can take a few more questions and then we can just uh go to the Victor cool anyone else uh I'm gonna get him at the moment okay cool yeah so uh okay uh let me okay so Daphne also has uh like uh like Daphne has mismatch like mismatch of like various problem paradigms so like Daphne also has like uh you can write data types in Daphne and you can write uh functions over that data type and then you can write like a specification on those data types and here you can see that in Daphne there's a data type which is uh which is uh three and it has two constructors if you think about constructor way uh one is leaf and one is north and like you can write a thing simple functions over uh these kind of data type and Daphne has construct per mass where you want to pattern as over these ways we have to construct those things and here they have written a uh a function which checks that whether uh whether it contains that uh value or not and one more thing I want to point out that Daphne has like a type parameter where like you can like since uh node value can be any type and Daphne has construct type parameter you can write that data and you know and then they they have written uh small very things and uh like for fill method where you write a tree and uh write on like write an array and you write on start method and it will try to fill uh that array with three elements starting with start array and yeah and like um one thing to note here is that uh like whenever a method uh tries to modify like uh like a heap allocated object you have to provide something called modified scores so like here you can see that array is one of uh like uh pointer based reference and Daphne has to say that um Daphne has to provide a specification set that that uh I wanted to modify this method uh if you don't provide it Daphne will uh allow to say that you are time to modify it but you haven't provided as a part of uh a specification that you want to modify it and uh one more thing I wanted to point out is that like all the post conditions and the conditions we have seen till now was was kind of not uh uh like uh uh like it doesn't like quantify over like whole lot of things but you can do it uh using for all cross so here uh what uh what you want to say that uh when uh uh when the feed is called uh the like um the the array elements uh from the start to end like contains those uh inductry and also before start uh index we haven't modified anything into the array itself so uh yeah so so if people want I can just give example in the editor also but if don't like people are seeing me typing on the editor I can just skip that nobody's bored we can cover that okay so okay let me cover this example because this is the last example I and other example is a class one uh which is very last uh so I will skip that instead of this one so one thing uh one thing uh which paper mentions and which also I want to highlight is that our uh post conditions only say that uh array element after start uh and up to and contains that tree element but it doesn't say like in which order it contains and like and other things you can say in general about this so like how strong you want to uh say about your specification is something which you have to decide and also you have to pay a price in the sense that you have to prove more stronger things and proving those things might be trickier than uh figuring out like this uh uh straightforward thing that it just contains so yeah before going like before jumping into the class example let's go through this tree example let's see uh let's uh write and then uh it has two constructors and there is more and there is a this is also free this value uh this is uh this is tree and so this is how like I have omitted the type parameter you can omit here uh you're going to write uh this uh in in the direct result and let's write a simple function which checks whether your value is contained into the tick or not here I also have to provide a type parameter and since this is a function I have to provide a type and then uh this need to be an expression in order to statement uh and his like I mentioned this thing because there are tricky cases in Daphne where it looks like you are writing um while it uh discussion but uh like very very discussion but that might be uh breaker might be doing a different thing because you have preconception of how uh things written in the statement so uh let's write uh in this case is the nice it is uh uh key and to check that whether uh whether that uh value contains in the tree you check whether this is the key is equal to very divided or uh left contains the key so this is like uh like pattern matching if you're familiar with pattern matching with other function angles it has pattern matching and you have to provide the pattern and then you have to provide various cases and then uh this all uh expression sort of of the same type which is the trend type yeah in this method we don't need any uh any precondition post conditions uh yeah that's one thing uh I want to mention that this this is a function and Daphne when Daphne reason about method it only uh knows about post condition about that method when um when you call that method but functions are uh visible to Daphne uh Daphne can unroll the functions and like since this is a statement whenever this function is called it can just um like spit out this code instead of like function and and reason about it itself and we will use this function to reason about method uh what this method is does is that it takes a tree and it takes an array and array should be of same time uh set type and then it takes something and it returns uh another interior uh uh and what I want this method to do is that it will fill uh array with uh elements of p starting from start and it will return the last index where up to where it has returned the array element uh so this looks fine we will just write like earlier methods that uh we will write without uh specification and try to write a specification and see how Daphne reacts and how we can help Daphne so uh that's like uh our function method will be the same structure where it will be matched and then depending on different match cases we will try to do things uh so in this case if we hit the loop mode then we just uh say that uh we haven't filled anything uh and our start our end is a start and uh and our specification was that from a start up to end extruding the end uh whatever the element will fill in the array will be part of the tree let's write the other thing where we just uh so here what we want to do is that like like since our specification is very uh liberal uh we can fill in either way and the way uh paper mentions and the way I'm going to do is that I will just try to fill entire elements with the left tree and then uh we'll try to fill uh if there is any element left then we'll try to fill with me and then uh uh uh try to fill with the right uh children of the tree so let's do that we will personally call it and then and then now if you want to check that uh like there is still um something left uh like uh there's there's a space left uh to fill so right and and then uh we can fill uh that uh element to tree and then uh we can just say that uh fill elements with uh a and and since we have fit up to end we have to put an end to this one so this is uh fit to build and Daphne was already company that you're trying to modify but he haven't provided any uh modify here because so you have to say that uh I want to uh modify see so I want to say that uh this method uh modifies and what is complaining is that it is out of range because because we know that and it doesn't end but it can be an end so this fit can turn something um uh uh let's say it turns a million and arrays of size 10 so so you have to like see that uh whatever you are uh joining is uh between start to and right uh now it is company again because you haven't uh specified what start can make uh can be like called or this method can call start with like negative number in that case uh not every number may be bigger than uh length of array and then in that case this but also not work so here you can have uh add a cross so as that uh caller can call only uh only with uh with a start um up to zero to uh and these are the like uh these are the specialization in the sense that uh like we are not uh accessing any array out of one but like we want strong condition that um um that uh whatever values we are turning are from the tree so we have to add that uh so this is how you write in something that for like a range of values you want to say something so what I want to say that uh to start to uh uh uh our our tree contains the element so this is how to do uh now the problem here is that okay now Daphne still not able to verify this thing uh like uh it is very hard to figure out like uh from looking into this core base why it is unable to verify but you can write a various assaults to figure out what Daphne knows and what Daphne doesn't know and the reason here is that uh here you are saying that uh between start with and um your um your uh array like whatever you are putting into array condition quickly but you are not saying anything about other array elements you are not saying that you you will not modify those array uh array elements so you have to also specify that for example let's say one because one call might put that tree element into the array but other other element like for example here I can add a clause that uh put random value into the array start uh maybe array 0 so in that way uh uh in that key like for example here I can say that put um um some random value into the uh into the last element of the array and the inside case that random element might not be the part of the tree so you have to uh write something called like I I don't want uh you want to write something called that uh that uh whatever I'm doing I am not modifying any array element uh between uh zero two start of that so this is uh this is uh you have to write it as a part of uh post condition and uh this is yeah you do it for example let me explain this whole part whole part means that uh whole part means that uh whole part means that uh whenever the method is called uh what was the value of a and after method returns uh what was the so this a uh expression will use the value of a after like in the last record and this whole a means that what was the value of a when the when the when the function was in before doing anything so this is uh way to do it I think so still not able to verify let me see uh right okay this is saying that in this part it is okay because uh let me see why it's not able to verify let me first check that whether I have written this oh I have written this so I have written this contents from I am checking like in left or right uh the key is part of left or right or not which is the like and you can see that Daphne is able to figure this strong like this crazy problem which I have to fix this time yeah yeah so this is how the like since this paper is very static and uh working with Daphne is very uh lively experience so I want to show like how it looks like and like I think we are on the last part of the paper so you can also specify the class in Daphne and uh like most of the things we have covered in uh uh till now one thing you can do in Daphne is that you can also write Bosch words Bosch word is something um which are which are state you wanted to hold on for verification but like these things you um these things are not required in current time program these are um something which is required because you want uh like you want to uh hold on to some previous state and you want to compare with uh with the new state and uh and it might be like before uh method called because like in method called you have uh passed out called all those kind of things you can just use Bosch word uh which is like you want to hold on to some state and you want to verify it so that's the additional thing and I think yeah that's all um that's all I have to cover yeah some cool uh quick note about like any any note about further reading and what uh yeah so I think uh Rustan has a like uh like a YouTube channel verification center like videos are like very old I think but uh he goes through uh goes through um few examples and and there is there is a paper also drafting papers but I think Rustan has also written a book which I just got just right now and but that book is draft and uh it's not you cannot find Amazon you have to uh you have to there's a independent publisher called Luru where um they are I think I can show you the book and this book goes into uh tell about like I don't I don't know whether you can see it or not it is called Quran proof uh and it goes through like all that it is yeah okay awesome awesome great I think uh a lot of people actually dropped off in the last 10 minutes uh so let's stop here today yeah I'll make the recording available and you know share on social media uh thank you so much the venture for covering this uh what I call it nerdy topic yeah thanks thanks for having me yeah it was like nice to talk to somebody which I'm doing like in my own and like talking to myself yeah yeah I think one one question came on Twitter is that uh are there any well-known use cases uh or well-known production use cases for Daphne like is anybody using it in production yeah imagine imagine using uh lots of formal verification tool and Rustam is currently working at Amazon and I think one of you know they have mentioned Daphne uh besides yeah yeah I think that uh in usually meetups like that question always comes up even for like arcane languages that haze it uh for production I'm not so big on that like I'm happy to just write uh Daphne Quran Saturday and then write some Ruby code on Monday for production yeah yeah one thing I also want to mention that like Emacs is not too bad I'm just using Emacs I think it's just to get started with using uh VS code and I think VS code has the like it's really friendly you can just use and there's a Daphne plugin and it will install Daphne itself I think maybe you might need to install a dot net runtime but that's extra thing you have to do but otherwise you are set to go got it okay awesome great uh I think uh that's a wrap for today I'm gonna


We really have good kids in this program and that's what I'm excited to continue to move forward with. For the most part, our fall was very productive and excited to keep this thing going in the spring. The biggest thing for me is this turf is tremendous.  I've really enjoyed being out here and getting outside and getting defensive work in. Having our shore stops throw across the diamond and our pitchers thrown outside. The conditions that we play in, let's be honest, in the spring it doesn't matter where you are. You're going to play in some cold weather and our pitchers have to get used to that and our haters have to get used to it. It's been good getting outside and getting some good work in. The biggest thing for me is that we get better every day and I know that's coach talk or generic but it's very much where this program, where we want to be in year one. Like I said, we have good kids and just trying to make sure they improve every single day is our biggest goal. You can't quantify wins and losses because there's going to be games where we get the right bounces and we don't get the right bounces. If we just get better, I think we'll be in a good spot towards the end of the year. I'm a defensive coach so that's probably the biggest thing I think as a team we're an offensive team. Combining those two things is very important. We have to play good defense. If we want to achieve championships in any team in the country, that's what they want to do. We do have to get better defensively and we have to throw strikes. If we do those two things, I think we'll be there because I know we're going to hit. We have a lot of guys coming back from last year's lineup that can hit the ball. I'm excited to coach those guys but also to get everybody better on the defensive side of the ball and throw a lot more strikes. I think we're going to have an exciting brand. We've got a lot of guys that can drive the ball all over the park and just good kids that are fun to cheer for. So that's what we're excited that the whole community comes out. Again, I've said that we were able to practice on a turf so people see baseball on the Owings Mills campus and we'll drive over to Greenspring and have some fun with us this spring.


Are you tired of watching boring old press releases? Then you've come to the right place, the right channel, the number one channel for CEO interviews and company overviews. Welcome to Rich TV Live, subscribe to our channel and make sure to hit the like button on our videos to help with the YouTube algorithm for more information and in-depth discussions and analysis, join our trading club at richpigsdaily.com and don't forget to subscribe and hit the bell for notifications to get alerted when our next CEO interview is released so you can discover the next 10-bagger. Hi, how are you doing today? I'm your host, Rich here on behalf of Rich TV Live with our very special guest, the chief investment officer of Vox Royalties, Spencer Cole. How are you doing today, Spencer? Very well, thanks, Rich. Thanks for having me today. Excited to have you guys on the show. You guys have been doing really well. We had you on the show earlier and we spoke to the CEO, very impressed with the CEO and the stock has moved up from 270 to 310 now and really it's just getting started. So I'm really excited to learn more, Spencer. Maybe you could tell us a little bit about yourself and how you got involved with Vox Royalties and what exactly is your role as chief investment officer? Absolutely, Rich. So my background is as a mining engineer, as you can tell from my unfortunate accent, I'm from Australia originally but now based in Toronto. Over the last 10 years, I've worked for some of the largest mining companies globally such as BHP and South32. About six or seven years ago, I co-founded a business called Mineral Royalties Online and we developed the world's largest database of mining royalties. And then subsequently, we merged that intellectual property into Vox about two and a half years ago. So that was how I came to be part of the Vox team. And now my role as chief investment officer is really, I guess, just ensuring that all of the new royalty acquisitions we do, you know, absolutely should the lights out from a rate of return perspective and that we truly understand the fantastic assets that we're investing in. Fantastic. Can you go through Vox Royalties' ability to find event-driven opportunities which I think is really special that create value for shareholders using your competitive advantages? Absolutely, Rich. So one of the key ways that we create value for shareholders is we use our technical management team, which is mining engineers such as myself and geologists as well. And we do all the technical due diligence on a mining asset that has a royalty on it. And what we look for is assets that have a huge number of sort of operational milestones and operational sort of momentum behind them. So for example, a mine that's just about to go into the final stages of feasibility or a mine that's just about the start construction. Because typically that's where we find we can price deals most aggressively in our favor. So our sweet spot is paying 20 to 40 cents in the dollar based on what the market would otherwise pay for a royalty. And then in three months time when the mine comes into production or it moves into the next key phase of its development all of a sudden that entry price of 20 cents in the dollar now looks close to the 10 cents in the dollar because the value of that royalty is re-rated. So in the past 12 months we've had five separate royalties that have moved into production. So royalties where we bought them right at the perfect time. And now they're generating huge revenue for our shareholders based on how we've timed those investments. I love your business model. Can you please explain to shareholders the growth in producing assets count and what that means to shareholders? Absolutely. So when we went public May of last year we only had one producing royalty asset. And that was a complaint of some investors. They said, how excited can I really get? You've only got one producing royalty asset. And we said, well, you know, hold that thought because we're buying assets that are right on the cusp of first production and first revenue. So as we stand today we've already grown that to five producing royalty assets. So our revenue has been increasing exponentially. Over the last three quarters, each quarter we've had about 500% quarter on quarter revenue growth. And that's sort of exponential revenue growth is set to continue because between today and the end of 2023 organically we expect to go from five producing royalty assets to 10 producing royalty assets and there's strong potential beyond that. So investors buying the Vox today are really getting in at the ground floor as we continue delivering on that sort of exponential growth curve without any additional capital committed. That is extremely impressive. I love your guys growth, quarter over quarter growth, new assets coming online, new royalties coming online. This is what investors want to hear. Now I want to talk about your recent press release because you guys acquired a very near term producing gold royalty for about 200,000 from a hearing aid company and the project owner just announced a construction award of 70 million. Can you explain that press release? Absolutely Rich. So this I guess demonstrates for your listeners and for our shareholders the leverage they get from buying into Vox and the leverage you get from owning these amazing gold royalties particularly. So you're absolutely right that in our global database of royalties we identified this sort of forgotten gold royalty that was sitting in the hands of a hearing aid technology company. Now listeners might say why the hell is a hearing aid company owning a gold royalty? Historically that had been a mining exploration company hollowed out as a shell company and then hearing aid technology company was dropped into it but we could see in our database no this company definitely holds this really attractive gold royalty. So we were able to negotiate a deal with them. We paid 200,000 for the royalty which gets us 1.5% of all the revenue from that gold mine. And as you said, the operators just announced they're committing 73 million dollars to building that gold mine. So from a $200,000 investment we're gonna make an absolute multiple on that investment as the asset comes into production over the coming 18 odd months. Wow, that is so impressive. Even 1.5% of that of 70 million would be my quick math be about a million bucks. Yeah, so the production rate is gonna be sort of approximately 50 odd thousand ounces of gold per annum. And so the rate of return on that investment should be very attractive for our shareholders. Very good, I love it. And we love to hear that word multiple as investors because we as investors and I'm an investor in our community is filled with investors from all over the world. We love finding a multiple and I believe this is a company that can give investors a multiple. Now, if there was one thing Spencer you could tell the shareholders that are watching or potential new shareholders that are watching something you could talk about or something you want shareholders to know today about Fox Royalties, what would it be? Look, I think Rich, beyond the organic growth that I highlighted before, we've got that benefit of just sitting back and watching that organic growth unfold over the coming quarters. I guess the cherry on the top of that is industry consolidation has really kicked off over the last few months. So in the last three months three separate of our competitors have been acquired. And so looking at I guess why people would want to acquire another royalty company, Vox stacks up really favorably, whether it's the huge organic growth in our revenue that we expect or also just the sheer volume of our royalty portfolio. We have 54 royalties. So even just the expiration royalties this year alone have over 160,000 meters of partner funded drilling on them. So we think we stack up very high on the potential takeover target list as the industry consolidates. But the important thing for us is we don't have a gun to our heads to enter into any transaction. We can sit back and watch that organic growth unfold and given us as management, we own 15% of the company. All of our families are heavily invested. I've got four of my brothers and sisters that are Vox shareholders. So I'm sure you they're very noisy shareholders every time things happen, they get on the phone to me. But we're in a really fantastic position where we don't need to do any transaction. But if a larger acquire knocks on our door, we serve at the behest of shareholders and we'll look for whatever's right for our shareholders. Spencer, we've got investors from all over the world that will be watching this interview and some of them are going to want to get in contact with you or the company. What is the best way for them to do that? Absolutely. So they can direct them to our website. So voxroilty.com. And then also if they've got any general inquiries, they can email us at info at voxroilty.com. If they want to ask me something directly or they want to hear my unfortunate Australian accent on the phone directly, they can email me at spencer at voxroilty.com. That's fantastic. Now I must remind you, everyone that's watching that Rich TV Live is strictly for information education purposes.  Please do your due diligence, do your research before you invest in anything that we talk about or discuss here on Rich TV Live. In saying that, I believe this is a company that is undervalued, under-appreciated, under-exposed. I think everybody needs to put vox, voxcf on their watches right now. We started covering this company at 270. Today it's at 310, slowly grinding up almost every single day, despite the fact that the market's been kind of weak. So this is a really good trade idea in my opinion. I'd love to know what you guys think. And remember guys, if you're not winning, you're not watching, we bring you the winners and we bring them to you first. I'd like to thank Spencer Cole, the Chief Investment Officer for joining us today. Thank you Spencer. And if you ever have any other big breaking news or anything you want to discuss, we'd love to invite you back on the show. Thanks so much for your time, Rich. And thanks to you listeners for tuning in. My pleasure. And like I said guys, if you're not winning, you're not watching, we bring in the winners and we bring them to you first. Thank you for watching everybody. Thank you Spencer. We'll talk to you soon. And we'll see you guys soon. Have a nice day everybody. This is Rich from Rich TV Live, signing off.


Hello, I am currently working as an editor for Djinnago. I have been working with them for the past two years. I have been working as an academic editor for the past four years. I have a master's degree in environmental sciences. My master's thesis focuses on hybrid energy systems. I am currently pursuing a PhD in materials science. My field of research is energy storage technology. I am focusing on supercapacity. Before I shifted my career to academia, I worked for several years as a design engineer in energy and water projects. I am passionate about everything because it gives me the opportunity to continue this scientific work through helping my parents' columns. It is my pleasure helping researchers meet their academic goals. Thank you.


Welcome to my second video on anatomy using the Wolfram language inside of Mathematica. The notebooks or the material that I'm going to make available for you are in the form of what Stephen Wolfram refers to as computational essays. It is a bit of a generic term and I suppose from my point of view what he means by that is that inside of Mathematica we have this beautiful notebook environment. Started in the late 80s when Mathematica started and today we see lots of copies of that in the form of our studio with our markdown files. We see that in the Jupyter notebooks that can use your browser in which you can code many languages. But this notebook environment where we write our code and we see the execution of our code, the results of our code really allows for this idea of a computational essay. Essay in the form of a narrative. Something that I can put down on a screen which I suppose I can eventually print so it can be on paper as well but let's keep it on this on a screen. A story that I can write. A narrative that I can weave to provide information to give information and knowledge and to write down the story of words and code and results with pictures, graphs etc. It is a beautiful something tangible that you create that you can share with others.  It is not that expensive to buy if you want to do that yourself. You can buy a yearly license for yourself and that really if you string together a few cups of coffee at your favorite coffee shop you're going to be able to afford this. You can also use the online version for instance the programming lab here. You can sign up for that free of charge and use it here and the web absolutely free. You can also sign up for this programming lab for a small fee every month. That will allow you a special desktop version to download and also to code right here in your browser online and store all your files online. There's so many ways that you can get involved in Mathematica without paying a single cent or for what you get actually pay very very little. So here we are on the Wolfram cloud. It's simply wolframcloud.com and this is the page that you'll see and you'll click on this programming lab and I'm not even going to sign in. I'm just going to show you what happens if we click on the free version. That is what you're going to see. You can watch a short video on this development platform. Again it allows you to sign up so that you can at least save your files. I'm not even signed up I'm not logged in or anything. I'm just showing you around for you to get an idea of this computational essay. And then if you click on create a new notebook this is what you're going to see. A beautiful coding environment. Your empty notebook here. You're going to see some advertisement on the bottom because I'm not signed in. I haven't signed up here and so you'll see this at the bottom. On the right hand side quite a few things for you to look at. The documentation is fantastic. There's one thing about the Wolfram language. It is the documentation. Everything that you need to know about the code is inside of a very easy to use and spectacular documentation. There's so many coding environments that we have today have such poor documentation that cannot be set of the Wolfram language. The documentation is excellent. There's also this elementary introduction to the Wolfram language. If we click on that that's a book written by Stephen Wolfram himself and you can click on all these topics on the left hand side all these chapters and you can just go through them and step by step teach yourself more about the Wolfram language. I'll put some links in the code below in the description below that will also show you some of my own courses that you can take if you want to learn more about the Wolfram language itself. I have a course just on the Wolfram language and one on statistics using the Wolfram language. So let's create another new document here. This is what it looks like and you can see it's already nicely formatted. I've put some suppose sections and titles in here and if I click on format here you see the formatting bar on the right hand side and you see also these marks on the side here. These are cells. Everything that you do inside of this computational essay in the Wolfram notebook Wolfram language notebook or Mathematica notebook exists in cells so I can highlight all of these cells here that says section 1 and then these bullet points and if I double click on those they actually just move up there and they are hidden away but I can see this little arrow here if you look closely you might not see this if you're viewing it on a small screen but if I double click on that it just all opens up and you can see if I want to add something new there's this horizontal bar I can just start typing the default would be to enter code but if I click on this little plus button it tells me the default is Wolfram language input code or I can just do plain text. There's free form or the Wolfram alpha query that you've actually seen before and but let's go for other style and if we move up to the top we'll see title and that's exactly how I got this big title up here subtitle is how I got that one and there's section one let's just do another section and if you view this on a large screen you'll see it actually says alt plus four so if you hold down alt or option key and hit four you'll get a new section and I'm just going to hit my down arrow and there's a new one let's just add some normal text plain text this is a line of text there we go simple as that let's do a new section and let's make it another section let's call this section three and you can see what we mean by computational essay I can create this beautiful almost word-like document but it is so much richer I can add so many things just to say anatomy plot 3d see the auto completion there I can just hit the tab key I can also hit this little down arrows and it'll show me what I have to put in there and I can also click on the little plus the I sign there I should say and then on the right-hand side we gonna see the documentation appear there we see the documentation and let's do this one left FEMA so arguments always go inside of square brackets I hold down control or command and hit the equal sign and I'm going to write left FEMA and I'm going to hit the tab key and it states that this is an anatomical structure do I want to accept that yes I do and I'm just going to close my square bracket hold down shift and enter or shift in return and there we go our FEMA and we beautifully I can also turn this FEMA around all the anatomy that I want to see right in front of my eyes the computational essay this idea of this notebook with these sections that exist inside of cells that I can just close down and open back up I can really weave a narrative here and produce this beautiful document and this is the document that we're going to look at next we're gonna talk about the clavicle it's going to be our first anatomical object that we're going to discuss and you can see the content that we're going to look at there this is inside the desktop version of Mathematica and you can see these cells have been collapsed and I can open them up by double-clicking here I'll close them again or on the desktop version there are these little markers here that allow me to open up and you can see what we have here text it's a document it's going to be exist that is going to exist in that you can download and you can really just read through the information there we're going to look at parts you can see text and code and the execution of the code a computational essay a beautiful beautiful document that you can use for so many things


NJRoot22.com here with a weekly supermarket roundup for December 7th. Most of these sales start on December 7th. The shop right goes till, I mean, starts on the 9th of December. So keep that in mind, okay? We're gonna try and blast through this real quick. But the only thing I thought was good at Kings this week, and by the way I'll remind you, we only shop here for convenience and buying things that are only on sale. They have a really good deal on the white cloud, paper towels and toilet paper. In our opinion, there are favorite paper towel and products and toilet paper products right now, and they're the cheapest price you'll ever get. $12.99 for two, which means they're $6.49 a pack. They've never been cheaper anywhere else, including ShopRite, the best I ever got at ShopRite was $6.99. And I think that's all there was in, oh, one last thing. Kings, we think they're prepared, food is pretty good. I wonder if anybody's ever used their catering. I don't know how the prices stack up. They're usually, you know, 10 or 20% in line with each other. I'm wondering if it's worth it to try their little chicken Wellington puffs or mini Franks in a blanket. That's something to think about. IGA, I didn't flip through it this week. We shop here, I'll remind you, because they're local and we want them to stay in business. They have convenient items and very good prepared food. But this week, just off the home page here, I think they have a good deal on chicken thighs, the best cut of chicken you can get, and they have a good deal on avocados as well. Bucke. Don't ever pay more than a buck. Aldi has them for $0.50 sometimes. Odd lot. I want it through job lot. Ocean state job lot. I want to remind you that the crazy deals are a very, very, very, very good thing. Just remember to buy things you need or can you use or can gift somebody and you'll make out. Don't buy something that you probably don't want or need just because there's a good deal on it.  Maybe some people are flipping these things on eBay to try and make some money. There is a possibility for some of these things to make some of your money back and just get free things. But never buy anything that you don't need. It's just truly a waste of time. I forget if there was something else in here that I... Oh, I wanted to see these. These are fusion forged knives. They look pretty high quality. I was at the store today and I didn't check them out. I am going to check them out the next time I go back either sometime this weekend. It can't hurt to have a good knife even though we have our those high-end German knives. We don't shop it, stop and shop. We just can't seem to get and bring them into the fold. They appear to have some good deals sometimes and they're very... I'm not going to talk about it. Let's talk about shop right here real quick. I guess now that holidays are coming around they have filet mignon, which is just another way of saying beef tenderloin on sale. They have like three or three or four different filet mignons on sale. They're the most expensive but yet most tender cut of meat you can get. They have their USDA whole beef tenderloins, 6 to 8 pounds. You're paying like 60 to 80 dollars pack of these standard run-of-the-mill. They have this. This is on sale here. I don't like nature's deserve. It's from Australia and they definitely have a different taste and some have argued to the contrary that the different taste is how meat's supposed to taste compared to the American meat and the jury's out for us on that. I don't know. Maybe I'm just not used to it. I mean some people say that about eating venison or you know I guess everything is an acquired taste. Another thing we notice is that they bring out the holiday stuff. You know sugar and morsels and chocolate. Are they appealing to people's desires or are they somehow nudging them and controlling them in a way as well? I think it's a little bit of both. I didn't see anything too fantastic and every week I talk about this. The fresh muts and ricotta cheese. It just seems like they're taking turns. Each week a new brand gets it. If it's Belgeoso or Galbani, just buy the ones that are on sale. It's basically what they're telling you. Of course the shop right and all these various cheeses are also on sale again this week but just a week or two ago they had to block the shop right chunk cheese which is very good for 99 cents and I got some rain check so I can get like eight blocks of cheese for the price of four.  Just get rain checks even if you don't plan on using it that week. You'll have the savings for a future date. Like I said it's all about chocolate. Look at these chocolates. Ferrero chocolate chocolate chocolate. I mean I guess yeah it's good for giving gifts but why is everybody shoveling chocolate extra? It's like Halloween Thanksgiving Christmas and then everybody buys gym memberships in January which they stop using three weeks later. It's like this vicious cycle of eating because the holiday tells you to eat which is which is bizarre. It's very bizarre. A lot of people are starting to break out of that cycle of seasonal eating but I would say good majority 70 to 85 percent of the country just just follows along and eats what's seasonally predicted or expected. I don't know. I mean you can hear I have a very conservative viewpoint on many things including food and the products that are available in mass and I think that's it. Oh they got a good deal on this Miss Myers and Mrs. Myers cleaners. I mean that's not a good deal but it's cheaper than normal and those are those are good cleaning products and here's I think an exceptional deal actually it's the Reynolds wrap the massive roll. It's like almost half price and it's normally like ten bucks or more for the big 200 square foot. That's on sale this week for for a very good price so if you if you want to stock up on that that now's a good time to do that if you have extra money and you're not don't have space or if you have space and I say no flu shot. I haven't had a flu shot in two decades and I have not had the flu. Go figure. I'm sure somebody's going to want to quarantine me one day and put me in some sort of bin because I didn't get the the medicine the little brain altering medicine they want uh want you to get. Your body your body's own immune system is what you want to uh to focus on not not some medicines. I don't know they got all their little various toys and half price batteries. You always keep an eye on that type of stuff. I save rechargeable batteries by the nickel metal hydride Amazon. Basics are are perfectly good and you'll get 500 charges or more out of them for and it comes out to being like like one twentieth the price over time and that's it for this week. Seven minutes and fifty five seconds with my intros and all that other stuff. Have a nice weekend and enjoy the upcoming holiday season as it ramps up into full gear.


What is the Activity Chooser? To add learning content to a Moodle course page, you use Moodle's Activity Chooser, which you can access by turning on the editing from the gear menu top right, and then in the section where you want to have your learning content, you click Add an Activity or Resource. This will bring up the Activity Chooser. If you don't see this link but instead you see two separate dropdown menus, check with your administrator. Let's click this link to take a look at the Activity Chooser and what it does. On the left is a list of activities. If we scroll down, we see that underneath is a list of resources. A resource in Moodle is static content which students would just read or look at or listen to. So for instance, if you're uploading documents and presentations, you'd use File or Folder. To present information directly, you'd use a page or you can use URL if you had a link to a website or an online file. Whereas, activities require students to interact with Moodle. They might submit work using an assignment or they might contribute to a forum discussion. The list can also include resources and activities which are not standard but which your Moodle admin has added as extras. The Learn Moodle site for instance has Big Blue button for web conferencing which isn't standard but which has been added. In order to find out about what each of these does, you click the Radio button next to it. Information then appears on the right telling you what it is, how to use it and useful teaching ideas. And if you click the More Help link, this takes you to Moodle's documentation with further information. You add an activity or resource by clicking the button and then clicking the Add button at the bottom or if you don't need to read the information, you can simply click twice on the button and that will take you to the setup screen.