WEBVTT 00:00.000 --> 00:13.160 So, this is working, seems like it, okay. 00:13.160 --> 00:19.960 So, we are on time, I believe, per minute, it doesn't matter. 00:19.960 --> 00:25.400 So, let's get started directly, and we are going to talk about some very technical topic, 00:25.400 --> 00:27.960 so I do expect some programming knowledge. 00:27.960 --> 00:33.560 Hopefully, I will make everything understandable, but if I don't, please feel free to ask 00:33.560 --> 00:37.840 questions afterwards, and if I make some mistakes, feel free to correct me on the spot, 00:37.840 --> 00:42.200 so that the recording gets the correct data. 00:42.200 --> 00:49.400 So, understanding liquid types, contracts, and formal verification, all with data. 00:49.400 --> 00:54.000 Nonetheless, even though this presentation is going to be using ADA, ADA Spark, I will 00:54.080 --> 00:56.760 explain the difference later. 00:56.760 --> 01:02.240 All the points I'm going to make, they should be translatable to other languages that also 01:02.240 --> 01:03.880 support these features, okay. 01:03.880 --> 01:04.880 That's my goal. 01:04.880 --> 01:10.160 That's the main goal to express these concepts in a general manner. 01:10.160 --> 01:14.880 And examples will be practical, I'm not a mathematician, I'm actually, I'm a kind of a linear 01:14.880 --> 01:17.360 work in nuclear sector. 01:17.360 --> 01:22.160 These things are not meant to, I'm not going to be too precise with whether something 01:22.160 --> 01:25.560 is a discrete type, a liquid type, whatever. 01:25.560 --> 01:30.080 No, things are going to be practical, and I'm going to show a bit of code. 01:30.080 --> 01:34.520 And the reason I'm going to do that is because of ADA, it is very readable, so I hope that 01:34.520 --> 01:39.000 everybody just by reading the code is able to understand all the concepts I'm about to 01:39.000 --> 01:40.000 use. 01:40.000 --> 01:46.080 Also, very interesting note, all the code I'm going to show you is valid ADA 2012. 01:46.080 --> 01:50.240 I'm 27 years old, that standard came 13 years ago. 01:50.240 --> 01:52.840 Half of my life, half of these features, being available. 01:52.840 --> 01:57.720 We think these concepts, these programming concepts are new, are fresh, no, they are not. 01:57.720 --> 02:02.080 They are very old, it's just that most programming languages just simply don't support 02:02.080 --> 02:04.800 them, which is kind of a something. 02:04.800 --> 02:07.080 So let's go directly into types. 02:07.080 --> 02:08.480 What are types? 02:08.480 --> 02:13.960 Normally when we think about types, we think about interiors, array, pointers, voids, whatever, 02:13.960 --> 02:18.880 you know, data, it's normally we think about of them as data. 02:18.880 --> 02:25.680 Maybe I understand them as data at the CPU level, 8 bits here, 64 bits there, and they 02:25.680 --> 02:33.560 are floating points, normally we focus on the information at the CPU GPU memory level. 02:33.560 --> 02:37.520 That's why higher level languages, they don't think of the, they normally don't have 02:37.520 --> 02:43.520 types or they just have numbers, and they abstract that information away. 02:43.520 --> 02:49.640 However, some newer programming languages have realized that types can be useful, very 02:49.640 --> 02:55.120 useful actually, they rust as an example with their optional type. 02:55.120 --> 03:00.000 They are using types not to just describe data, but to describe program flow. 03:00.000 --> 03:05.040 In the case of the optional type, it describes something that may get you some data, or 03:05.040 --> 03:09.040 something that may get you no data, for example, a network request. 03:09.040 --> 03:12.840 If you make a network request, any fails, you get nothing in return. 03:12.880 --> 03:17.600 If you can model that behavior at the type system in your language, and the compiler 03:17.600 --> 03:23.000 will check, will force you to check those two different stages, so that you don't miss 03:23.000 --> 03:25.200 mistakes, which is great. 03:25.200 --> 03:31.040 But when we talk only about it, only about information, most programming languages are still 03:31.040 --> 03:36.720 default to generate bits in your CPU, which is kind of a shame. 03:36.720 --> 03:42.120 So when we ask ourselves questions like, hey, this variable, great, it's an unsighted, 03:42.120 --> 03:45.000 bit into here, and it's value 11. 03:45.000 --> 03:47.800 Is that a good grade for us student to get in a test? 03:47.800 --> 03:49.320 Is that a bad grade? 03:49.320 --> 03:55.080 We don't know, it's just unsigned bit into here, and it has the value of 11. 03:55.080 --> 03:59.200 French people will say, yes, that's a passing grade, German people, or Spanish people will 03:59.200 --> 04:01.480 say, no, that's not possible. 04:01.480 --> 04:02.480 And that's the problem. 04:02.480 --> 04:05.240 We have no context for our data. 04:05.240 --> 04:11.680 People think, oh, low level, you have to work directly against the CPU, which is not true. 04:11.680 --> 04:16.720 We need the type system, and I believe this are called discriminated types, or discrete, 04:16.720 --> 04:18.720 whatever. 04:18.720 --> 04:21.360 In a data, we describe the real world data. 04:21.360 --> 04:23.080 We actually work with. 04:23.080 --> 04:25.040 That is a huge improvement. 04:25.040 --> 04:29.800 So we can describe what is good data, what's not bad data. 04:29.800 --> 04:35.800 We can have a tower of dives, for example, in this case, the grade is number from 0 to 10, 04:35.800 --> 04:41.400 and we have a subtype, which is just a normal type that's completely compatible, fail 04:41.400 --> 04:43.720 grade, which is from 0 to 4. 04:43.720 --> 04:47.560 So if I ask you, is three passing or failing grade? 04:47.560 --> 04:51.720 You can tell me the answer, just by looking at the information. 04:51.720 --> 04:56.520 We can refine things, obviously, this is the Spanish grading system, so we have decimal point 04:56.520 --> 04:57.520 numbers. 04:57.520 --> 05:00.320 Yes, we have decimal point numbers in ADA. 05:00.320 --> 05:03.800 This is a fixed point time, most smaller problem languages, those support these types, 05:03.840 --> 05:09.040 which is kind of a huge shame, especially if you are working with money and things like that. 05:09.040 --> 05:10.040 Very soft. 05:10.040 --> 05:14.600 And a lot of people see this, and they say, oh, ADA is very verbose. 05:14.600 --> 05:20.320 I just need an unsigned ADA, but the thing is, this is useful, because we can do stuff 05:20.320 --> 05:21.320 like this. 05:21.320 --> 05:27.000 A is steep, rowing 38 in a failed grade, and the answer is yes. 05:27.000 --> 05:30.200 We can't reason about our information at the code level. 05:30.280 --> 05:35.640 Think about data validation, it just becomes trivial, it's wonderful. 05:35.640 --> 05:40.040 But of course, some people may say, hey, what about efficiency? 05:40.040 --> 05:43.640 ADA is an ADA supposed to be a low level programming language for embedded systems, 05:43.640 --> 05:46.120 and the thing is, the compiler does the heavy lifting for us. 05:46.120 --> 05:50.600 And if you want to have control of the beat level, and I say beat level, not by the level, 05:50.600 --> 05:52.280 you can do that very easily in ADA. 05:52.280 --> 05:55.400 If I have time, I have some backup slides for that. 05:55.400 --> 05:58.840 And you can play around with your code in the compiler explorer, 05:58.920 --> 06:04.040 and see if they're simply easy to get efficient or not, I can tell you that. 06:04.040 --> 06:06.760 But careful with your optimization flux, by the way. 06:06.760 --> 06:13.240 Nonetheless, someone may ask a question, AFER, you're talking about modeling real world data, 06:13.240 --> 06:16.280 and ranges, and things like that. 06:16.280 --> 06:21.320 Good, they are good, but what about some other data, some more complex data, 06:21.320 --> 06:26.840 some more refined data, like even numbers, or prime numbers, they cannot be represented 06:27.160 --> 06:30.520 with a generic range. 06:30.520 --> 06:34.440 How does ADA do any of that? 06:34.440 --> 06:38.440 Well, let's understand the data we are trying to represent. 06:38.440 --> 06:41.640 Normally, data has some kind of definition. 06:41.640 --> 06:45.400 In the case of even numbers, or prime numbers, 06:45.400 --> 06:50.200 their definition would be for even numbers, for example, numbers that are divisible by two. 06:50.200 --> 06:55.000 And we can very easily transform any definition into an AFER statement. 06:55.000 --> 06:59.160 If a number is divisible by two, then it is a prime number. 06:59.160 --> 07:03.240 Same thing for prime numbers, although the definition is a little bit more complex. 07:03.240 --> 07:09.160 If a number is divisible, it's only divisible by one, and itself, then it is a prime number. 07:09.160 --> 07:14.120 We can transform pretty much any definition into a logical statement. 07:15.640 --> 07:20.920 Can we put that logic that reasoning as part of our type definition? 07:20.920 --> 07:24.920 Can we make types with logic attached to them? 07:24.920 --> 07:26.360 types with logic? 07:26.360 --> 07:29.960 Logically qualified, liquid types. 07:29.960 --> 07:32.040 So, that's it. 07:32.040 --> 07:35.640 Liquid types are types with logic in a simple way. 07:35.640 --> 07:38.280 I don't want to get too academic about it. 07:39.560 --> 07:41.240 So, how would we go about it? 07:41.240 --> 07:48.600 Well, let's say even numbers are just numbers, but we now need to express what we just said. 07:48.680 --> 07:52.600 And Neda, we are going to do that with the Withky word, dynamic predicate. 07:52.600 --> 07:55.720 Predicates are just a way of introducing logic to stuff. 07:55.720 --> 07:58.360 And the Withky word is an incredibly powerful A-Daky word. 07:58.360 --> 08:00.360 I don't want to express, explain. 08:00.360 --> 08:04.600 But nonetheless, all languages, all different languages have their own kind of syntax. 08:04.600 --> 08:09.000 One of the reasons I'm using Neda to explain these topics, it's very readable. 08:09.000 --> 08:11.720 Some other languages I encourage you to take a look at them. 08:11.720 --> 08:14.920 They tend to be very symbolic, heavy, syntax heavy. 08:14.920 --> 08:17.320 In Neda, it's just English prose. 08:17.320 --> 08:18.920 So, we just say that. 08:18.920 --> 08:23.240 Dynamic predicate, and we write down the definition of our data. 08:23.240 --> 08:29.640 Even modular true, so that when we take the remainder of the division, we get zero. 08:29.640 --> 08:37.400 Now we have truly uneven number, and we can get the odd numbers basically for free with that. 08:37.400 --> 08:38.600 What about prime numbers? 08:38.600 --> 08:40.360 Well, oh, sorry. 08:40.440 --> 08:47.400 And the things we just did before, like, testing for our data and data validation, 08:47.400 --> 08:53.160 now becoming intrinsic to the program flow of our execution. 08:53.160 --> 08:57.640 So, if I say my even number is to, yes, everything's fine. 08:57.640 --> 09:02.040 But if I say, A, I'm going to sign the value three to my even variable. 09:02.040 --> 09:08.760 Oh, no, if you compile A-Daky with assertions enabled, you will get a runtime exception. 09:08.760 --> 09:13.960 In this part, as we will see in formal proofs, your code will not even compile. 09:13.960 --> 09:15.720 Oh, that's very interesting. 09:15.720 --> 09:19.800 So, now incorrect program state truly becomes incorrect. 09:20.760 --> 09:24.360 And we can still do testing for validity of data. 09:24.360 --> 09:26.520 It's three and even the answer is false. 09:26.520 --> 09:29.640 Once again, you can test this in compiler explorer if you want. 09:29.640 --> 09:32.680 But without prime numbers, well, we just write the definition. 09:32.680 --> 09:35.240 Obviously, it's a little bit more refined. 09:35.240 --> 09:37.080 Obviously, it's a little bit more complex. 09:37.080 --> 09:39.640 I will let you check whether that definition is correct. 09:39.640 --> 09:45.480 And it is, by the way, using some funny A-Dak, A-Dak doesn't have a lot of 09:45.480 --> 09:46.520 undefined behavior. 09:46.520 --> 09:49.880 So, even incorrect ranges are defined to have a behavior. 09:49.880 --> 09:57.720 But anyway, so, and the thing is, we don't even have to express all the properties of our data 09:57.720 --> 10:01.400 as part of our type definition. 10:01.480 --> 10:07.480 If you have your typical e-sballied data function or ballied data functions, 10:07.480 --> 10:12.440 you can just pop them into your definition to your predicates. 10:12.440 --> 10:14.200 You don't even have to rewrite your code. 10:14.200 --> 10:17.640 Just pop them in, pop them in, and that's it. 10:17.640 --> 10:22.200 Also, liquid types in A-Dak are known as type contracts. 10:22.200 --> 10:25.240 In other languages, they are also known as that, just letting you know. 10:26.600 --> 10:28.200 I know what you're thinking. 10:28.920 --> 10:34.440 A-Dak, this is useful for academics, and that's why liquid types are used by academics. 10:34.440 --> 10:39.800 Just look at your examples, even numbers, prime numbers, our cryptographers. 10:39.800 --> 10:44.920 This is useless for real-world programming, because real-world programmers do other stuff. 10:44.920 --> 10:46.520 Well, let's take a look at this. 10:46.520 --> 10:50.280 Imagine we have a data structure, and we are tracking some temperature. 10:50.280 --> 10:54.280 It could be some logging system of your server. 10:54.280 --> 10:57.640 It could be a financial institution, tracking some stock prices. 10:57.720 --> 10:59.800 And we have a timeframe, for example, days. 10:59.800 --> 11:01.000 It could be milliseconds. 11:01.000 --> 11:06.040 It could be your, I don't know, measuring some electricity in your outlet, every hour, or whatever. 11:08.040 --> 11:12.120 And we have a high value current value and low value. 11:12.120 --> 11:16.840 We always want to keep track of current state and the bounce of our data. 11:16.840 --> 11:20.280 And somewhere in the code, maybe written by us or by someone else, 11:20.280 --> 11:22.440 we just want to update the current value. 11:22.440 --> 11:25.160 And we do serve, no, this is the very typical thing. 11:25.160 --> 11:26.680 We are just doing an assignment. 11:27.480 --> 11:29.880 Oh, no, we just introduced a bug. 11:29.880 --> 11:30.520 Can you tell? 11:31.720 --> 11:35.000 Just doing an assignment and created a data corruption bug, 11:35.000 --> 11:38.120 because we forgot to update our values. 11:38.120 --> 11:40.760 What if the temperature we're measuring in our garden? 11:40.760 --> 11:43.960 The current temperature is, I don't know, 30. 11:43.960 --> 11:48.040 And we didn't update the high value from before, which was maybe 28. 11:48.040 --> 11:52.120 Does it make sense to have a data structure whose high value is 28? 11:52.120 --> 11:53.560 The current value is 30. 11:53.560 --> 11:56.520 And the lower value is, I don't know, 25. 11:56.520 --> 12:00.120 No, we just corrupt our data structure. 12:00.120 --> 12:02.360 Very simply, just by doing a simple assignment. 12:04.360 --> 12:05.240 And here's the thing. 12:05.240 --> 12:09.000 If we know the properties of our data, the high value has to always be high. 12:09.000 --> 12:11.400 The current higher than the current value. 12:11.400 --> 12:15.720 And the current value has to always be greater or equal to the lower value. 12:15.720 --> 12:17.240 Why don't we write that down? 12:17.240 --> 12:19.160 That's just a liquid type. 12:19.160 --> 12:24.360 We express the nature of our data, how our data behaves, 12:24.360 --> 12:27.480 or is related to each other. 12:27.480 --> 12:28.760 We just write it down. 12:28.760 --> 12:30.040 And it's not a common. 12:30.040 --> 12:31.560 This is actual code. 12:31.560 --> 12:33.960 And if you compile a data with assertions, 12:33.960 --> 12:37.080 you will get a runtime error once you return the data. 12:37.080 --> 12:41.080 It's a data allows intermediate incorrect data states. 12:41.080 --> 12:42.760 In a spot, you are not allowed to do that. 12:42.760 --> 12:47.640 And you will get a proof error if you write this code. 12:47.640 --> 12:50.760 What about sorting algorithms? 12:50.760 --> 12:53.960 Or, sorry, searching algorithms that are very efficient. 12:53.960 --> 12:56.360 And they need to work on sorted data. 12:56.360 --> 12:57.560 How can we represent that? 12:57.560 --> 13:00.120 In most programming languages, you just cannot. 13:00.120 --> 13:03.960 You just pass a generic array and you hope it's sorted. 13:03.960 --> 13:07.800 In good programming, you create a new type that's sorted. 13:07.800 --> 13:13.960 And it's only returned by procedures that use sorted data. 13:13.960 --> 13:14.840 But we can do better. 13:14.840 --> 13:18.200 We can express the nature of sorted data directly 13:18.200 --> 13:21.160 as the type definition with a liquid type. 13:21.160 --> 13:24.600 We introduce the logic of what it means to be sorted 13:24.600 --> 13:26.920 as part of the type definition. 13:26.920 --> 13:27.960 That's wonderful. 13:27.960 --> 13:31.800 That's very powerful. 13:31.800 --> 13:35.000 And I want to address one big comment that I now 13:35.000 --> 13:37.160 I'm going to get in the questions and answers. 13:37.160 --> 13:41.160 A for another, you're example with data, with the temperature. 13:41.160 --> 13:43.800 Yeah, that's has been solved since like the 80s, 13:43.800 --> 13:47.480 by using the get-in-setter pattern, object-oriented. 13:47.480 --> 13:50.040 If your data has some kind of behavior, 13:50.040 --> 13:51.160 you just make it private. 13:51.160 --> 13:52.760 You don't let people modify it. 13:52.760 --> 13:55.160 And you create a function that does the correct 13:55.160 --> 13:57.480 modification to your data. 13:57.480 --> 14:01.400 Liquid types are nothing-border. 14:01.400 --> 14:02.360 But here's the thing. 14:02.360 --> 14:03.720 Yes, you would be right. 14:03.720 --> 14:06.040 And this example would indeed give you 14:06.040 --> 14:08.040 better code reviews, actually. 14:08.040 --> 14:09.560 But here's the thing. 14:09.560 --> 14:11.640 For example, in this case, object-oriented programming, 14:11.640 --> 14:13.720 which is how most people would do that today, 14:13.720 --> 14:15.400 it's a whole new programming paradigm, 14:15.400 --> 14:19.400 and liquid types are yours types that have been enhanced. 14:19.400 --> 14:21.880 It has a high-sad data, which basically 14:21.880 --> 14:26.280 nukes the three things you do with data, read, write, and modify. 14:26.280 --> 14:28.680 You just basically destroyed the nature of data. 14:28.680 --> 14:31.080 And it requires you to create an API. 14:31.080 --> 14:34.920 So now the problem of adding data, it's on you. 14:34.920 --> 14:36.360 And here's the thing. 14:36.360 --> 14:39.000 Is that said, a function blocking? 14:39.000 --> 14:40.600 Is it writing to a file? 14:40.600 --> 14:43.880 That's forbidden in a lot of cases for hyper-performance computing. 14:43.880 --> 14:44.600 Did you know that? 14:44.600 --> 14:48.040 Oh, did the person that called the set-up function knew that? 14:48.040 --> 14:49.800 Was that documented? 14:49.800 --> 14:53.560 If it wasn't, you have got a bunch of other issues, 14:53.560 --> 14:56.040 because normally the APIs are opaque. 14:56.040 --> 14:58.920 People don't look how they are implemented. 14:58.920 --> 15:00.760 And that's a problem. 15:00.760 --> 15:02.280 Liquid types are your types. 15:02.280 --> 15:04.680 Powerful types, but these types. 15:04.680 --> 15:08.200 They are wonderful for instrumenting and debugging your code. 15:08.200 --> 15:11.480 I actually can tell you that I enjoy debugging data code, 15:11.480 --> 15:14.280 which doesn't happen with any other language. 15:14.280 --> 15:17.240 And they will allow us to do formal verification, 15:17.240 --> 15:18.520 as I will explain later. 15:18.520 --> 15:21.160 And here's the thing, the wonderful thing about liquid types. 15:21.160 --> 15:24.680 They can just go access with the rest of other programming paradigms. 15:24.680 --> 15:28.280 If you do OP functional, they just refer to data. 15:28.280 --> 15:31.320 So anything that works with data, all programming paradigms, 15:31.320 --> 15:33.720 basically, they can just use it. 15:33.720 --> 15:35.000 They are not in compatible. 15:35.000 --> 15:37.400 And if in case you don't like this example, 15:38.040 --> 15:40.680 you can use the limited key work, whatever. 15:40.680 --> 15:42.040 It is a great language. 15:42.040 --> 15:43.880 So let's go directly into functional contracts. 15:43.880 --> 15:46.280 And I'm going to be much faster here, 15:46.280 --> 15:48.840 because here's the thing, what are the programs? 15:48.840 --> 15:51.400 Perums are things that take some inputs. 15:51.400 --> 15:54.120 They process those inputs, and they generate some outputs. 15:54.120 --> 15:55.800 It can be a simple function. 15:55.800 --> 15:58.760 It can be whole program, whatever. 15:58.760 --> 16:01.320 And we've been talking about data, about liquid types, 16:01.320 --> 16:07.160 about being declarative, about explaining what our data actually is. 16:07.160 --> 16:10.840 So we've been focusing on the inputs and the outputs, 16:10.840 --> 16:12.760 and about their properties. 16:12.760 --> 16:14.200 And here's the thing. 16:14.200 --> 16:16.840 Someone could ask the very simple question. 16:16.840 --> 16:19.880 Hey, could we apply the same principles, 16:19.880 --> 16:24.440 but instead of just the data, the actual execution of our program? 16:24.440 --> 16:25.240 Can we do that? 16:25.240 --> 16:28.520 Can we add contracts to our code? 16:28.520 --> 16:31.480 Dipes to our code, just like we do with types? 16:31.480 --> 16:32.120 And yes, there is. 16:32.120 --> 16:33.880 Yes, that's functional contracts. 16:33.880 --> 16:36.120 So let's go directly to a general example. 16:36.120 --> 16:41.880 Imagine we have a stack package where we can push data in, 16:41.880 --> 16:43.960 and we can pop data out. 16:43.960 --> 16:48.440 Well, we all mostly know that that is the end years. 16:48.440 --> 16:51.160 What happens if you push too much data into stack? 16:51.160 --> 16:52.760 Well, you just go to the buffer overflow. 16:52.760 --> 16:55.320 What happens if you pop too much data into a stack? 16:55.320 --> 16:57.800 Well, underflow. 16:57.800 --> 17:02.920 How do we know what's the behavior of our functions when that happens? 17:02.920 --> 17:04.920 If that happens at all? 17:05.000 --> 17:06.600 Is it going to be suspended? 17:06.600 --> 17:09.160 Well, we would need to look into the functions, 17:09.160 --> 17:13.240 and see if it's guarded or not, or what they are doing. 17:13.240 --> 17:16.280 Simple, if we are very worried about our users, 17:16.280 --> 17:19.480 mistreating our functions or our data structures, 17:19.480 --> 17:21.240 we can do explicit guarding. 17:21.240 --> 17:23.640 And if someone tries to push too much data, 17:23.640 --> 17:27.480 we can say, hey, sorry, you cannot do that. 17:27.480 --> 17:29.400 And raise an exception through an exception. 17:29.400 --> 17:31.800 And in that would be the case of failure. 17:31.800 --> 17:33.800 But can we do better? 17:33.800 --> 17:38.280 Would it be correct to push more data than what's available? 17:38.280 --> 17:44.280 No, so why don't we say that as part of our function declaration? 17:44.280 --> 17:46.840 And we do that with functional contracts. 17:46.840 --> 17:49.800 So for example, in the push function, we say, 17:49.800 --> 17:52.760 with, once again, that key word of header, 17:52.760 --> 17:57.080 pre, and pre is a short form of pre-condition. 17:57.080 --> 18:00.920 Before you are allowed to call this function, 18:01.080 --> 18:03.160 this stack must not be full. 18:03.160 --> 18:06.280 You are not allowed to call this function if this stack is full. 18:06.280 --> 18:09.080 Now we don't no longer have to do explicit checking our function. 18:09.080 --> 18:11.400 That's guarded by the pre-condition. 18:11.400 --> 18:13.240 By all the properties that have to be true 18:13.240 --> 18:15.880 before the function gets executed. 18:15.880 --> 18:17.800 And we also have post-conditions. 18:17.800 --> 18:22.840 What happens after the function has been called, in the case of the push function, 18:22.840 --> 18:25.080 well, the size of this stack must increase. 18:25.080 --> 18:30.760 By one, we must have added some data to our data structure. 18:30.760 --> 18:35.800 That seems obvious that we don't even know how complex this function is 18:35.800 --> 18:37.560 or what it is doing in between. 18:37.560 --> 18:40.760 It could be a three-line code, a code bit, 18:40.760 --> 18:42.600 or it could be 5,000 lines of code. 18:42.600 --> 18:46.040 The monologics, the monolog, function of the G lip C. 18:46.040 --> 18:47.560 It's about 5,000 lines of code. 18:47.560 --> 18:48.360 Did you know that? 18:48.360 --> 18:50.760 It started with this allocating some EC memory? 18:50.760 --> 18:51.400 No, no, no. 18:51.400 --> 18:53.560 These things can become extremely complex. 18:53.560 --> 18:56.040 And we don't care how complex they are. 18:56.040 --> 19:00.280 These properties are going to hold a regardless of what you do. 19:00.280 --> 19:02.680 And we can annotate our code to do that. 19:02.680 --> 19:04.840 Also, if you would like to see the full answer, 19:04.840 --> 19:07.720 to how to correctly program and stack, 19:07.720 --> 19:12.840 you go to this repository to the platinum reusable stack, 19:12.840 --> 19:16.280 it's going to be a lot more than what you think. 19:16.280 --> 19:19.320 There is a lot of implicit behavior that people think 19:19.320 --> 19:21.800 and that needs to be guarded against. 19:21.800 --> 19:25.480 And I'm here just showing you pre-conditions post-conditions. 19:25.480 --> 19:29.080 But real world examples, they are complex. 19:29.080 --> 19:32.600 Like global state contracts, like data dependency contracts, 19:32.600 --> 19:33.560 et cetera, et cetera, et cetera. 19:33.560 --> 19:35.480 This is a real piece of example. 19:35.480 --> 19:39.880 What happens when we move some vectors or some data 19:39.880 --> 19:41.880 to another place to another vector? 19:41.880 --> 19:44.360 Well, these are all the things that need to hold. 19:44.360 --> 19:49.720 What happens when we do an insertion of one bit of data into a vector? 19:49.720 --> 19:51.800 You think that's simple? 19:51.800 --> 19:53.640 No. 19:54.840 --> 19:58.920 These code, by the way, is part of a Spark formal containers. 19:59.240 --> 20:02.280 A Sparkleet is a formally verified library that you can just use. 20:02.280 --> 20:04.040 It's under Apache version 2. 20:04.040 --> 20:08.040 It's created by the people that dissect the critical systems. 20:08.040 --> 20:10.440 These things are robust. 20:10.440 --> 20:15.480 They are not only memory saved, they have no runtime exceptions. 20:15.480 --> 20:18.440 They know runtime issues, they're correct handling 20:18.440 --> 20:20.600 of the exceptions, everything. 20:20.600 --> 20:24.360 And talking about safety critical systems and things like that. 20:24.360 --> 20:28.680 Wouldn't it be great if when we program 20:28.680 --> 20:32.760 something, we could know that it works as we expect it? 20:32.760 --> 20:38.840 Wouldn't it be great if when we program something that we know that's doing what we hope to do? 20:40.040 --> 20:45.800 And that our clients can be sure that our program does what they want us to do? 20:46.680 --> 20:49.000 Wouldn't that be great even before we compile it? 20:49.000 --> 20:52.680 Like in Rust, like for example, the borrowed sugar will make sure that your program 20:52.680 --> 20:54.920 doesn't have any memory issues before it compiles it, 20:54.920 --> 20:56.600 because thanks to the borrowed sugar. 20:56.680 --> 20:59.480 Can we do all the checks before we compile that? 21:01.240 --> 21:04.440 Well, yes, but there are a lot of checks that we need to run. 21:04.440 --> 21:09.160 Like memory errors, program flow errors, unexpected arithmetic errors. 21:09.160 --> 21:12.600 There is a lot that people just simply forget about. 21:12.600 --> 21:15.000 And we can we prove that? 21:15.000 --> 21:22.360 Oh, proof. Provers. Yes. Provers are basically compilers, but instead of creating a assembly, 21:23.240 --> 21:29.400 they do all the checks I mentioned before, and they give you a thumbs up or a thumbs up, 21:29.400 --> 21:32.120 and they tell you whether your program has issues. 21:32.120 --> 21:35.240 And those issues are can be very varied, okay. 21:35.240 --> 21:39.560 Rust World Checker is for example, a Prover for correct memory management. 21:40.920 --> 21:44.600 And some other Provers are better wars at some different things. 21:44.600 --> 21:46.600 For example, TLA plus, I've seen it. 21:46.600 --> 21:50.200 We've been used more for like concurrency issues and things like that to detect those. 21:51.160 --> 21:57.960 And some Provers are interactive and they can walk you through like your program and see if your 21:57.960 --> 21:59.720 program has some issues somewhere. 21:59.720 --> 22:05.240 Other Provers like Spark, which is the formal subset of Ada, which no longer is that much of a subset, 22:06.280 --> 22:10.440 will do so automatically. You just create your code, press bottom, go and grab a coffee, 22:10.440 --> 22:15.400 and the Prover will tell you, hey, you have an overflow here that you hadn't thought about. 22:15.400 --> 22:16.200 It's wonderful. 22:17.080 --> 22:20.680 And the way these things work is that they have some Provers. 22:20.680 --> 22:26.680 The Provers have some like Perms known as SMT, Theorem Provers and things like that, 22:26.680 --> 22:32.280 like set three, Alter, I go CVC5, that they will get your code, they will analyze it, 22:32.280 --> 22:36.440 and they will tell you where what could go wrong and things like that. 22:38.440 --> 22:41.640 So do people actually use this in the real world? 22:42.680 --> 22:45.640 Most people think of oh yes, like cryptography people. 22:45.640 --> 22:48.440 But real world parameters don't need these techniques. 22:48.440 --> 22:52.920 The answer is yes, people are working in an operating systems. 22:53.960 --> 22:59.480 When you need a reliable operating system that's just not going to break, you use these techniques. 23:00.680 --> 23:03.240 Liquid types, contracts, formal proofs. 23:03.240 --> 23:05.160 Of course, yes, cryptography. 23:05.160 --> 23:10.600 And one of the beautiful things about Ada, you can just work on it on embedded systems. 23:10.600 --> 23:12.280 A lot of other Provers don't do that. 23:13.080 --> 23:16.040 And a lot of people are worried about performance. 23:16.840 --> 23:20.360 I would recommend you click on the optimized for performance link there. 23:20.360 --> 23:23.000 The guide that created this cryptographic library, 23:23.000 --> 23:27.480 optimized it for performance while maintaining full proof correctness. 23:28.040 --> 23:32.280 But not only that, we use a ton of software daily that we are just not aware of, 23:33.000 --> 23:34.280 that we just expect to work. 23:35.160 --> 23:36.840 Are we sure it's just going to work? 23:38.040 --> 23:41.160 Our Perms constantly parsed JSON or XML. 23:41.240 --> 23:42.200 Are they going to work? 23:42.200 --> 23:46.760 How many times have we seen security issues every time someone gives a model, 23:46.760 --> 23:49.960 form thing, a model form, jpeg or whatever? 23:50.520 --> 23:53.240 Quite okay, image format. 23:53.240 --> 23:57.720 Someone who we actually have here created a library, 23:57.720 --> 23:59.880 it's formally verified to work on it. 23:59.880 --> 24:02.520 And it doesn't matter if you feel it incorrect data, 24:02.520 --> 24:04.600 an incorrect, malformed image. 24:04.600 --> 24:06.120 It's just not going to break. 24:06.120 --> 24:08.680 It has been verified to do that level. 24:08.680 --> 24:12.920 So, as a conclusion, liquid types and contracts allow us to express 24:12.920 --> 24:16.120 the properties of the nature of our code and our data, 24:16.120 --> 24:21.160 and they document and give meaning to our program at the code level. 24:21.160 --> 24:24.840 They serve us instrumentation, the bug ability of our code, 24:24.840 --> 24:29.720 and they allow us create very robust code and for proofs. 24:29.720 --> 24:34.040 And the formal proofers, the formal verification of our code, 24:34.040 --> 24:38.040 gives us the assurance that things are going to work as we expect them. 24:38.120 --> 24:41.720 They are going to be memory correct, they are going to have no exceptions. 24:41.720 --> 24:45.000 Or if they have exceptions, they are going to be handled correctly 24:45.000 --> 24:47.640 that we are not going to have overflows underflows 24:47.640 --> 24:50.360 incorrect data management, et cetera. 24:50.360 --> 24:51.320 And they are wonderful. 24:51.320 --> 24:55.400 And especially Spark is a wonderful teacher because it has a counter example, 24:55.400 --> 24:57.880 flag that you can pass it and it will explain you 24:57.880 --> 25:01.880 and walk you through how you got something wrong, which is wonderful. 25:03.080 --> 25:07.080 So, and just a bit about Ada, the reason I love Ada 25:07.160 --> 25:09.640 is because it has all this features I have mentioned, 25:09.640 --> 25:13.960 but you can also work on embedded systems we feel without operating systems. 25:13.960 --> 25:16.360 And Ada supports a ton of architectures, 25:16.360 --> 25:19.320 it's low level, high level, it's very readable, 25:19.320 --> 25:22.760 you can interrupt with C code, it's wonderful. 25:22.760 --> 25:26.840 Yes, it's not perfect, some issues are part of the community 25:26.840 --> 25:32.360 and the ecosystems, some limitations are part of the language by design 25:32.360 --> 25:34.600 in order to get these robustness. 25:35.000 --> 25:39.960 But thank you, and other questions how much time we have for those? 25:41.000 --> 25:44.440 One minute for questions, oh, sorry about that, thank you. 25:52.440 --> 25:54.680 So one quick question only, yes? 25:54.680 --> 25:56.360 When you use these steps, you said, 25:56.360 --> 26:00.680 to what degree are they verified at a compound time versus a runtime? 26:01.560 --> 26:05.880 Oh, so, thank you, I mentioned that with Ada, 26:05.880 --> 26:08.600 we have the beautiful thing of being able to, 26:08.600 --> 26:12.040 oh, let me repeat the question for the online people, 26:12.040 --> 26:14.520 what are the advantages on the differences of runtime 26:14.520 --> 26:17.800 and a proof time of being able to select those, no? 26:19.480 --> 26:22.600 We are the ones by versus a compound line. 26:23.880 --> 26:24.920 Well, are the difference. 26:24.920 --> 26:29.240 So, at runtime, in Ada, you can select 26:29.320 --> 26:32.200 if you just write your program, you can select full runtime correctness 26:32.200 --> 26:35.240 with that, it comes to a course of the runtime. 26:35.240 --> 26:41.000 And Ada is a little bit lenient in some of the features. 26:41.000 --> 26:45.880 You can do a runtime like temporary, you can have temporary incorrect 26:45.880 --> 26:47.640 to state if you so wish. 26:47.640 --> 26:49.480 In Proof, Proofers are very strict. 26:49.480 --> 26:54.040 They will not allow you to have any intermediate incorrect data 26:54.040 --> 26:57.960 or state, and the runtime comes with the cost 26:57.960 --> 27:01.560 of, well, they actual checks, 27:01.560 --> 27:03.320 where they can not place a runtime. 27:03.320 --> 27:07.000 The size of the objects of the program is going to be larger, 27:07.000 --> 27:11.320 but you gain the bug ability and the traceability 27:11.320 --> 27:14.920 of your programs, that's why it's so we sit to the bug Ada. 27:14.920 --> 27:16.920 You just run it, run it on another bug, 27:16.920 --> 27:20.040 you just tell it to catch all assertions, to catch all exceptions, 27:20.040 --> 27:23.800 and you just close your eyes and let the bug refine it. 27:23.800 --> 27:27.720 But the proofer, it will be a bit slower, noticeably slower. 27:27.720 --> 27:31.240 But once it's been proven, you can just 27:31.240 --> 27:34.440 trust the compilation of your code and go ahead with it 27:34.440 --> 27:36.920 and trust me it fully. 27:36.920 --> 27:41.480 So there are no more time because we have an issue. 27:41.480 --> 27:44.120 Nonetheless, go ahead and write it to me in my email if you 27:44.120 --> 27:45.160 also want. 27:45.160 --> 27:49.560 And I, reminder, yes, Ada allows you to do very low level 27:49.560 --> 27:50.760 control of data. 27:50.760 --> 27:52.040 So thank you. 27:52.040 --> 27:57.880 APPLAUSE