WEBVTT 00:00.000 --> 00:12.800 I know my title is a little bit contentious maybe, but I'm a rest developer, I'm allowed 00:12.800 --> 00:14.280 to say that. 00:14.280 --> 00:16.080 So, who am I? 00:16.080 --> 00:17.080 I'm Alia Bequet. 00:17.080 --> 00:20.200 I'm a rest-competitive developer, I've been now for 10 years. 00:20.200 --> 00:21.800 I came to us actually because of Ada. 00:21.800 --> 00:25.200 Before that, I was doing Ada. 00:25.200 --> 00:29.320 Well, I've been doing rest for 10 years now, and my Ada's a little bit rusty, so it's very 00:29.320 --> 00:30.320 interesting. 00:30.320 --> 00:39.200 But I still coded if you know, and then, anyway, it's talk is not about rest-of-engellism. 00:39.200 --> 00:41.280 It's the out-of-way around, more. 00:41.280 --> 00:46.720 It's just showing where we're currently at, because we've been doing a lot of work on getting 00:46.720 --> 00:53.880 rest ready to use and take the grid of systems more, and yeah, so what have we been doing 00:53.880 --> 00:56.080 here? 00:56.080 --> 00:58.360 A bunch of topics. 00:58.360 --> 01:04.000 The unsafe keyword is to think that, basically, what in Ada is the by convention unchecked 01:04.000 --> 01:05.000 keyword. 01:05.000 --> 01:10.040 It's not really a keyword in Ada, but it's what you used to say, like, this thing is probably 01:10.040 --> 01:11.040 going to be dangerous. 01:11.040 --> 01:15.000 You should read a documentation otherwise, if you think it's going to blow up. 01:15.000 --> 01:16.680 We use have some problems there in rest. 01:16.680 --> 01:20.520 I think we've gotten through all of them now, so I'm going to check, give this small 01:20.520 --> 01:27.520 intro there, generic packages, modules, really cool in Ada, rest, yeah, crickets, safety 01:27.520 --> 01:32.680 certification, going to go into details there, and we have contracts now. 01:32.680 --> 01:37.880 They're coming, they're not merged yet, fun, but PR's open and almost ready to be merged. 01:37.880 --> 01:38.880 And it's up-type. 01:38.880 --> 01:44.200 That's kind of my baby that I've been working on for like, whatever, 10 years, and we've 01:44.200 --> 01:50.200 gotten there, and so I'm going to most of the talk is going to be about sub-typeing. 01:50.200 --> 01:54.120 So, uncheck first, unsafe. 01:54.120 --> 01:58.840 This is an example of code that you can write in rest up to a few months ago, that would 01:58.840 --> 02:03.800 have been totally fine, compiling, and your program would have blown up, because you created 02:03.800 --> 02:08.320 a malloc function, and malloc is a weak symbol in most code that you have out there. 02:08.320 --> 02:13.520 So if you just define a random malloc function with a literal symbol name malloc, you are 02:13.520 --> 02:17.520 now the owner of the malloc function, whatever you write in there is malloc, and so if you 02:17.520 --> 02:21.600 just do something like random integer, well, your code is probably going to blow up because 02:21.600 --> 02:25.240 somebody is going to call malloc and dereference it, and well, that's something to happen. 02:25.240 --> 02:29.480 Anyway, we fixed that you now have to actually specify unsafe somewhere in there before 02:29.480 --> 02:32.840 you didn't have to, and I'm blowing up a program without writing unsafe. 02:32.840 --> 02:35.040 Yeah, no, not good. 02:35.040 --> 02:38.360 So we fixed that. 02:38.360 --> 02:39.840 Generic packages and modules. 02:39.840 --> 02:45.520 If you write a generic package and rest, you get this error message, like it's so unsupported, 02:45.520 --> 02:48.880 even the diagnostics, no, no, what you're talking about, and rest is actually famous for having 02:48.880 --> 02:55.600 good diagnostics, so anyway, I'm going to fix that soon, but just fixing the diagnostics, 02:55.600 --> 02:58.040 not actually implementing any feature. 02:58.040 --> 03:03.760 Safety certification, we are safety certified, we have a application of, not for, well, yeah, 03:03.760 --> 03:04.760 fair seen. 03:04.760 --> 03:08.960 Fair seen is used in safety code systems, you're allowed to actually use your stuff 03:08.960 --> 03:14.040 in, like, cars and whatnot, at least in Germany now, I don't know about other countries. 03:14.040 --> 03:18.160 And there were some little bit of drama, like, this was used to be an interoperable 03:18.160 --> 03:21.800 with ADACORE and fair systems. 03:21.800 --> 03:27.320 It is now not drama happened, people quit stuff like happen, I don't know if people quit 03:27.320 --> 03:33.200 because of this, but anyway, cool, we have this now, and it's being distilled, being developed 03:33.200 --> 03:36.960 for extended, and it's always up to date with, like, the current rest version, maybe, 03:36.960 --> 03:41.640 like, six weeks behind or something, but yeah. 03:41.640 --> 03:51.480 So, contract, contract and rest are similar to contracts before, like, ADAC, what's it 2012. 03:51.480 --> 03:55.240 When we did, we can contract actually in a language. 03:55.240 --> 03:59.960 It's basically attributes, which are more similar to how you have random comments somewhere, 03:59.960 --> 04:04.600 except that the language will actually now check these attributes, and you can specify 04:04.600 --> 04:06.960 arbitrary pre and post conditions. 04:06.960 --> 04:10.960 They're not actually formally checked in the way that a spark checks them, but we have 04:10.960 --> 04:16.920 to Connie formal checker for rest, which is similar to spark, it has all this S&T solvers 04:16.920 --> 04:21.200 in there, it gives you diagnostics, it creates counter-examples and whatnot. 04:21.200 --> 04:25.640 It's not fully complete yet, but it works for a lot of rest code, and it's being used 04:25.640 --> 04:30.200 to, like, prove small, cut rest code as completely free of runtime exceptions. 04:30.200 --> 04:33.520 So, that's cool. 04:33.520 --> 04:37.640 And, well, the thing I want to actually want to talk to you all about, after giving you 04:37.640 --> 04:41.080 this small update, pattern types. 04:41.080 --> 04:50.640 Pattern types in rest are similar to ADAC, except what we normally have in rest is just 04:50.640 --> 04:56.120 like concrete types for, like, a non-zero U32 that's like an actual type in standard library. 04:56.120 --> 04:59.760 You don't specify, like, I just want my integer to not have zero. 04:59.760 --> 05:04.320 What you do is you use this building type, and you actually define this type yourself. 05:04.320 --> 05:08.880 You can't do a non-ten U32, that just doesn't exist in rest yet. 05:08.880 --> 05:14.800 And, similar for pointers, there's a non-nal generic type that you can define for any kind 05:14.800 --> 05:20.480 of pointer type, and it will give you a non-nal pointer, but this is just a standard 05:20.480 --> 05:21.480 library type. 05:21.480 --> 05:25.480 It has a lot of magic in there to make it work, but it's not something you as a user 05:25.480 --> 05:29.320 will actually be defining yourself. 05:29.360 --> 05:33.440 It's kind of side, so the rest of the stuff is actually well explainable. 05:33.440 --> 05:36.920 In rest, types, type aliases are not strong. 05:36.920 --> 05:42.560 Not like ADAC where you have, like, a concrete different type, rest, the left side and 05:42.560 --> 05:45.360 the right side, even though they are called different things, they're specified the 05:45.360 --> 05:48.280 different lines of code and whatever, they're just the same type. 05:48.280 --> 05:52.120 Like, rest will not actually know that bar exists. 05:52.120 --> 05:55.760 It will just know that, like, there's a U32 here now. 05:55.800 --> 06:00.880 It's not a pre-processor, but it will just transparently make this disappear. 06:00.880 --> 06:05.600 It's just a help for you to not write the code twice and be able to easily change 06:05.600 --> 06:07.040 like type definitions. 06:07.040 --> 06:15.840 So, that keep that in mind when I'm going into my examples that are following patterns. 06:15.840 --> 06:21.840 Noterside, before we go into actual pattern types, patterns in rest are similar to the 06:21.920 --> 06:25.840 whole case patterns that you have in ADAC. 06:25.840 --> 06:31.200 You can match on something and then, like, this is almost the same syntax. 06:31.200 --> 06:36.480 The rest formative just doesn't put spaces between the dots, otherwise, it's pretty much 06:36.480 --> 06:37.640 the same thing. 06:37.640 --> 06:42.720 And there's other syntaxes, like, the ore pattern, which is, like, do separate things. 06:42.720 --> 06:47.440 Like, this is a cat dog or bat, and then if it's one of these, then you go into 06:47.440 --> 06:50.800 dot arm when others go into the rest. 06:50.960 --> 06:55.280 These kind of patterns are what we actually want to use for specifying subtypes and rest, 06:55.280 --> 07:03.040 because we already have to concept of something, matches, some specific subsection of that type, 07:03.040 --> 07:06.960 and we just want to reuse that because we don't want to duplicate another system. 07:06.960 --> 07:10.320 So, that's what we're basically trying. 07:10.320 --> 07:15.040 One cool thing about rest, you can specify patterns that are matched together. 07:15.040 --> 07:20.480 So, here, I'm matching on two variables at the same time, and it's required to the first variable 07:20.560 --> 07:23.600 is in range one to ten, and second variable is dot or cat. 07:23.600 --> 07:31.040 Then we go into this arm, and if it's 10 to 20 and dot or cat or bat, then we go into this arm. 07:31.040 --> 07:37.200 So, you can combine multiple types and check them at the same time together. 07:37.200 --> 07:42.000 And that's something that we want to use in our pattern types too. 07:42.000 --> 07:46.800 This also works in data, but you need to specify more complex bounds there. 07:47.680 --> 07:49.680 It's not like a building thing directly. 07:49.680 --> 07:52.240 You need to do these front-hand checks as far as I can tell. 07:55.600 --> 07:57.040 So, how would this look? 07:57.040 --> 08:03.520 We had the earlier example of non-zero, and now my plan for the very far future is that the standard 08:03.520 --> 08:08.720 library will actually replace the non-zero U32 type with this type of alias. 08:08.720 --> 08:15.840 It will literally be a U32 is one dot dot, so a U32 that starts at one and can be any value after that. 08:16.320 --> 08:20.720 And similar thing for null pointers, we don't use the not key word because we are less 08:20.720 --> 08:24.560 using such rules and short of stuff, so we do not bang, and then no. 08:25.360 --> 08:29.200 This syntax might completely change, depends on what the language team decides, but 08:29.840 --> 08:30.960 something like that will happen. 08:32.000 --> 08:37.040 And so, we can define those types that are really building into the standard library. 08:37.040 --> 08:38.880 So, what else can we do? 08:38.880 --> 08:46.400 First, I already mentioned that pattern types do not do strong typing, so you do not get 08:46.400 --> 08:50.800 separate types. If you do the same type definition twice, it will be exactly the same thing. 08:50.800 --> 08:55.680 If you say U32 is one dot dot something, another person defining in a completely different 08:55.680 --> 08:58.240 library completely somewhere else, same thing, same type. 09:00.240 --> 09:05.040 And for the language knows about you, pattern types are not actually doing sub-type 09:05.600 --> 09:11.360 pattern types, only curves between each other, like the compiler will insert conversions, 09:11.360 --> 09:16.480 but there will be no actual type system sub-type in where the types are actually like 09:16.480 --> 09:19.600 sub-type stuff each other like what happens with lifetimes and rust. 09:19.600 --> 09:24.080 Lifetimes do a lot of sub-type thing, but we are trying to keep it to lifetimes and not 09:24.480 --> 09:28.480 to explode that more. That might change in a future, but for now we are trying to get it. 09:28.480 --> 09:38.720 So, how do you actually create a pattern type? Up to this week, earlier this week, what you 09:38.720 --> 09:45.520 have to use was a transmute, like unsafe code to convert an integer to the actual sub-type. 09:45.520 --> 09:49.760 And now, what you can do is you can just specify literal, just like an eight-hour, 09:49.760 --> 09:53.760 you specify literal, and assign it to your sub-type. And the compiler will just check, 09:53.760 --> 09:57.040 this is literally actually in range for that sub-type, and if it's evidence and it will 09:57.040 --> 10:02.000 just merge it, and if it's not, then it will actually emit an error. On the other hand, 10:03.200 --> 10:07.760 if you're converting a variable, so you declare a variable here, and you convert that, 10:07.760 --> 10:12.080 you need to currently use transmute, there's no good conversion in eight-hour, you literally just 10:12.080 --> 10:19.280 use the type, and it will do a run-type check for you. But we're working on that, and what we 10:19.280 --> 10:25.920 want to do is, thanks for the previous presentation, I stole your stuff. Here's a great type, 10:25.920 --> 10:31.360 which is 1 to 6, and a passing grade, which is 1 to 5, German passing grades, anyway. 10:31.360 --> 10:36.480 And you have a variable of type grade, however you get that value. What you then want to do is, 10:36.480 --> 10:43.600 do you convert that grade with tri-from into a passing type, and then you get an option back, 10:43.600 --> 10:48.160 because either the conversion succeeds, then you get the thing in your option sum, or it doesn't 10:48.160 --> 10:51.920 see getting into a non-new, don't actually get the value. If it doesn't succeed, you don't get 10:51.920 --> 10:57.920 a value. Important stuff, good that ADA and Rust are getting this right in contrast to other languages. 11:00.960 --> 11:06.320 And there's lots of more stuff that I want to do. These things don't work yet at all, but 11:06.320 --> 11:12.160 Rust patterns. I want to basically, if you can write a pattern in Rust, in like a match, 11:12.160 --> 11:16.800 I want you to be able to write a pattern type for it. So having combinations of like a type where 11:17.760 --> 11:23.120 the U32 must be between 1, 0 and 100, and the string must be limited to specific things. And 11:23.120 --> 11:28.400 this is in combination. You cannot go out of this, these belong together, and maybe even at some 11:28.400 --> 11:35.040 point have constraints where like 0 to 50 means cake and 50 to 100 means fruit or something like 11:35.040 --> 11:40.080 that, where you can make more complex combinations of that. I want to, if you can specify the pattern, 11:40.080 --> 11:44.560 I want you to be able to write a pattern type, and we have a good plan for forgetting there. 11:46.800 --> 11:50.240 So, I'm almost out of time, so let's go to the summary. 11:52.240 --> 11:56.240 Genetic modules completely to do not happen any time soon, don't wait for it. 11:56.880 --> 12:02.080 Contracts are working progress, they're happening pretty fast, and I think they are already supported 12:02.080 --> 12:06.880 in the county model checkers, so we'll just get them basically for free as a static check. 12:07.760 --> 12:11.840 Head and type, I'm working on them. If you want stuff, complain to me. I'll try to make 12:11.840 --> 12:16.000 stuff work. My next step is idiomatic conversion, so to try from that you saw earlier, 12:16.560 --> 12:21.760 and where we've cut up, we have safety certification, and we're some, by default, pretty much 12:21.760 --> 12:26.400 module loads, some, something that's back said we're fixing, but like, that's a compiler back, 12:26.400 --> 12:30.000 not an actual language bug. Thanks, questions. 12:30.880 --> 12:34.880 APPLAUSE 12:39.120 --> 12:43.760 So, the matching on, let's write a constraint, 12:43.760 --> 12:49.680 induce certain strings, kind of scares me. Why can't we just have the, 12:49.680 --> 12:54.880 like, having it in just the generic types that implement the rate, and like, if, like, 12:54.960 --> 13:00.880 the rate for me, probably, that you're a library, or whatever, because, ideally, 13:01.440 --> 13:06.960 whenever I see, it can be these strings, it gives me, maybe, like, helps for clients. 13:08.400 --> 13:12.400 OK, the question is, why can we actually match some strings, 13:12.400 --> 13:17.040 and say, like, this could be like cake or fruit or something, and what, why isn't there, 13:17.040 --> 13:22.400 like, some better system, I think? Yeah, I don't actually know it's a hard topic to do something 13:22.400 --> 13:27.360 better, they're really like, you can do runtime checks, similar to, to the ADA runtime checks, 13:27.360 --> 13:31.920 or you can do this oralist thing. We don't really have a better concept. Like, there's ideas 13:31.920 --> 13:35.520 for integrating, like, RECX into, like, matches or something like that, but it was, like, 13:35.520 --> 13:39.040 very far off, and I don't know if we're going to do that or anything at all. 13:39.600 --> 13:43.360 There might be better ways to do this. I don't really know about it. I'm happy to talk about 13:43.360 --> 13:46.000 ideas, but, yeah, I don't know. 13:46.080 --> 13:53.840 Considering that you feel that Rust has caused out in terms of safety certification, 13:53.840 --> 13:58.320 my question is, how in Rust do you prove the absence of runtime checks? 13:59.680 --> 14:03.200 The question is, how do you prove in Rust, the absence of runtime exceptions? Well, similar to 14:03.200 --> 14:08.880 all, we have Spark and Ada, we have Connie and Rust. It is a working progress, but it does 14:08.880 --> 14:13.600 actually do the same kind of checking, and it is actually being used for pretty much the same 14:13.680 --> 14:15.840 things. With one minute, it's a one more question. 14:18.800 --> 14:23.520 Thank these subtitles. Will I be able to explain Spectre's subtitle in a country, like, 14:23.520 --> 14:29.280 first reference, that I also have the, what's the, what's the generic type? Will I be able to 14:29.280 --> 14:37.920 pass into subtitle? Will this have any problems? Or, uh, because I'll feel like that you get this 14:38.320 --> 14:46.880 subtitle. Can you? Can you? I assume I've got a subtitle. Yeah. 14:46.880 --> 14:52.000 Raise one to five, and I expect that you said two, but I'd be able to pass it on to the subtitle. 14:52.000 --> 14:57.760 Okay, the question is, if you have a subtitle, can you use that anywhere where you can use the 14:57.760 --> 15:04.400 normal base type of that? And the answer is, you can outside of generic context first, because 15:04.480 --> 15:08.720 there's implicit conversion from subtitles to the base type, because every subtitle is a valid 15:08.720 --> 15:14.640 version value of the base type. But, um, if you're using generic context, um, we're currently 15:14.640 --> 15:20.080 figuring out how to implement traits for subtitles, um, and, and how to implement, like, implicit 15:20.080 --> 15:24.400 conversions there. Um, we're not using actual subtitle, so we need to figure out something better, 15:24.400 --> 15:28.800 uh, but it might be that the answer is all this. We actually need full on subtitle, uh, we don't 15:28.880 --> 15:34.880 know yet. I have a couple of minutes. Cool. More questions. Over there. 15:44.080 --> 15:51.040 The question is, uh, how do you specify, uh, to some mentally equal, but, uh, with different, 15:51.040 --> 15:56.640 uh, representation, like, to two types was the same representation, uh, for the, for the, 15:56.720 --> 16:01.360 use and language by the different layout representation, and, uh, I don't actually think you can do that. 16:08.800 --> 16:12.800 The question is, uh, can you use constant functions and contracts? Right now you can just use any 16:12.800 --> 16:20.400 runtime code, uh, because they just run time checks, um, contracts are working progress, and we're 16:20.400 --> 16:24.320 figuring out the details there, but the simplest thing was to simply make them just run time checks 16:24.400 --> 16:28.160 and to start in the end of function of the function right now, and we'll figure out the details as we go. 16:40.960 --> 16:46.080 Yeah. So the question is, why is this in text highlighted, not actually catching, there's, 16:46.080 --> 16:50.080 uh, pre-conditions and post-conditions in the, in the, in the contracts. And, uh, the thing is the 16:50.080 --> 16:54.000 contracts are attributes, and attributes don't actually support expressions in them, and they 16:54.000 --> 16:58.320 were some bunch of hacks going on there. Like basically the attribute is a proch macro that generates 16:58.320 --> 17:03.840 some super secret internal rest-replication language, um, and, uh, we don't actually know where 17:03.840 --> 17:07.680 this is going yet. It might actually end up just being surface language syntax that actually 17:08.640 --> 17:13.440 doesn't use attributes, uh, but like this is working progress and the language team would like us 17:13.440 --> 17:20.080 to be more using weirters syntax to start with. So today we don't prescribe what the language 17:20.080 --> 17:25.040 is going to go and, and, and up with, and not get people used to some, something that actually 17:25.040 --> 17:26.240 looks like they want to use it in the end. 17:27.200 --> 17:48.640 Yeah. So the question is, um, if you, for example, use a non-zero type inside an option, what you get is, 17:48.640 --> 17:53.600 the same size as the non-zero type, because the option knows like, oh, there's a zero missing, 17:53.600 --> 17:59.360 I can just use that for my non-value. And, um, uh, the pattern types actually, that's the first thing 17:59.360 --> 18:03.600 I implemented before. I implemented anything else in pattern types, implemented if you do like 18:03.600 --> 18:08.720 zero to 100, all the other possible values of your integer are now for three for other 18:08.720 --> 18:14.560 enums to take, to put their, uh, discriminants in. So you can actually nest like 50 options inside 18:14.560 --> 18:18.960 each other, and in the middle there's a zero to 100, and, um, that will just be the same size 18:19.040 --> 18:19.920 as the original value. 18:26.240 --> 18:31.360 Well, the pattern types, oh, so the question is, can you do, it's supposed to say like, which bits are supposed 18:31.360 --> 18:35.280 to be there and which not, and the answer is simply the range that you're specifying that's 18:35.280 --> 18:39.600 the value range and everything else is invalid. And, uh, if you specify like multiple ranges, 18:39.600 --> 18:44.800 right now, the limitation is it will just pick the biggest space of invalid values and use that 18:44.800 --> 18:48.240 for everything. It will not actually preserve all the invalid spaces. 18:50.080 --> 18:52.560 That's cool. Time. 19:02.240 --> 19:05.920 For I'm going to be in a whole way for questions if people want to back me about stuff, 19:05.920 --> 19:09.840 uh, have you talked about rest? Talk about data and stuff. Um, grab me.