So, this is working, seems like it, okay.
So, we are on time, I believe, per minute, it doesn't matter.
So, let's get started directly, and we are going to talk about some very technical topic,
so I do expect some programming knowledge.
Hopefully, I will make everything understandable, but if I don't, please feel free to ask
questions afterwards, and if I make some mistakes, feel free to correct me on the spot,
so that the recording gets the correct data.
So, understanding liquid types, contracts, and formal verification, all with data.
Nonetheless, even though this presentation is going to be using ADA, ADA Spark, I will
explain the difference later.
All the points I'm going to make, they should be translatable to other languages that also
support these features, okay.
That's my goal.
That's the main goal to express these concepts in a general manner.
And examples will be practical, I'm not a mathematician, I'm actually, I'm a kind of a linear
work in nuclear sector.
These things are not meant to, I'm not going to be too precise with whether something
is a discrete type, a liquid type, whatever.
No, things are going to be practical, and I'm going to show a bit of code.
And the reason I'm going to do that is because of ADA, it is very readable, so I hope that
everybody just by reading the code is able to understand all the concepts I'm about to
use.
Also, very interesting note, all the code I'm going to show you is valid ADA 2012.
I'm 27 years old, that standard came 13 years ago.
Half of my life, half of these features, being available.
We think these concepts, these programming concepts are new, are fresh, no, they are not.
They are very old, it's just that most programming languages just simply don't support
them, which is kind of a something.
So let's go directly into types.
What are types?
Normally when we think about types, we think about interiors, array, pointers, voids, whatever,
you know, data, it's normally we think about of them as data.
Maybe I understand them as data at the CPU level, 8 bits here, 64 bits there, and they
are floating points, normally we focus on the information at the CPU GPU memory level.
That's why higher level languages, they don't think of the, they normally don't have
types or they just have numbers, and they abstract that information away.
However, some newer programming languages have realized that types can be useful, very
useful actually, they rust as an example with their optional type.
They are using types not to just describe data, but to describe program flow.
In the case of the optional type, it describes something that may get you some data, or
something that may get you no data, for example, a network request.
If you make a network request, any fails, you get nothing in return.
If you can model that behavior at the type system in your language, and the compiler
will check, will force you to check those two different stages, so that you don't miss
mistakes, which is great.
But when we talk only about it, only about information, most programming languages are still
default to generate bits in your CPU, which is kind of a shame.
So when we ask ourselves questions like, hey, this variable, great, it's an unsighted,
bit into here, and it's value 11.
Is that a good grade for us student to get in a test?
Is that a bad grade?
We don't know, it's just unsigned bit into here, and it has the value of 11.
French people will say, yes, that's a passing grade, German people, or Spanish people will
say, no, that's not possible.
And that's the problem.
We have no context for our data.
People think, oh, low level, you have to work directly against the CPU, which is not true.
We need the type system, and I believe this are called discriminated types, or discrete,
whatever.
In a data, we describe the real world data.
We actually work with.
That is a huge improvement.
So we can describe what is good data, what's not bad data.
We can have a tower of dives, for example, in this case, the grade is number from 0 to 10,
and we have a subtype, which is just a normal type that's completely compatible, fail
grade, which is from 0 to 4.
So if I ask you, is three passing or failing grade?
You can tell me the answer, just by looking at the information.
We can refine things, obviously, this is the Spanish grading system, so we have decimal point
numbers.
Yes, we have decimal point numbers in ADA.
This is a fixed point time, most smaller problem languages, those support these types,
which is kind of a huge shame, especially if you are working with money and things like that.
Very soft.
And a lot of people see this, and they say, oh, ADA is very verbose.
I just need an unsigned ADA, but the thing is, this is useful, because we can do stuff
like this.
A is steep, rowing 38 in a failed grade, and the answer is yes.
We can't reason about our information at the code level.
Think about data validation, it just becomes trivial, it's wonderful.
But of course, some people may say, hey, what about efficiency?
ADA is an ADA supposed to be a low level programming language for embedded systems,
and the thing is, the compiler does the heavy lifting for us.
And if you want to have control of the beat level, and I say beat level, not by the level,
you can do that very easily in ADA.
If I have time, I have some backup slides for that.
And you can play around with your code in the compiler explorer,
and see if they're simply easy to get efficient or not, I can tell you that.
But careful with your optimization flux, by the way.
Nonetheless, someone may ask a question, AFER, you're talking about modeling real world data,
and ranges, and things like that.
Good, they are good, but what about some other data, some more complex data,
some more refined data, like even numbers, or prime numbers, they cannot be represented
with a generic range.
How does ADA do any of that?
Well, let's understand the data we are trying to represent.
Normally, data has some kind of definition.
In the case of even numbers, or prime numbers,
their definition would be for even numbers, for example, numbers that are divisible by two.
And we can very easily transform any definition into an AFER statement.
If a number is divisible by two, then it is a prime number.
Same thing for prime numbers, although the definition is a little bit more complex.
If a number is divisible, it's only divisible by one, and itself, then it is a prime number.
We can transform pretty much any definition into a logical statement.
Can we put that logic that reasoning as part of our type definition?
Can we make types with logic attached to them?
types with logic?
Logically qualified, liquid types.
So, that's it.
Liquid types are types with logic in a simple way.
I don't want to get too academic about it.
So, how would we go about it?
Well, let's say even numbers are just numbers, but we now need to express what we just said.
And Neda, we are going to do that with the Withky word, dynamic predicate.
Predicates are just a way of introducing logic to stuff.
And the Withky word is an incredibly powerful A-Daky word.
I don't want to express, explain.
But nonetheless, all languages, all different languages have their own kind of syntax.
One of the reasons I'm using Neda to explain these topics, it's very readable.
Some other languages I encourage you to take a look at them.
They tend to be very symbolic, heavy, syntax heavy.
In Neda, it's just English prose.
So, we just say that.
Dynamic predicate, and we write down the definition of our data.
Even modular true, so that when we take the remainder of the division, we get zero.
Now we have truly uneven number, and we can get the odd numbers basically for free with that.
What about prime numbers?
Well, oh, sorry.
And the things we just did before, like, testing for our data and data validation,
now becoming intrinsic to the program flow of our execution.
So, if I say my even number is to, yes, everything's fine.
But if I say, A, I'm going to sign the value three to my even variable.
Oh, no, if you compile A-Daky with assertions enabled, you will get a runtime exception.
In this part, as we will see in formal proofs, your code will not even compile.
Oh, that's very interesting.
So, now incorrect program state truly becomes incorrect.
And we can still do testing for validity of data.
It's three and even the answer is false.
Once again, you can test this in compiler explorer if you want.
But without prime numbers, well, we just write the definition.
Obviously, it's a little bit more refined.
Obviously, it's a little bit more complex.
I will let you check whether that definition is correct.
And it is, by the way, using some funny A-Dak, A-Dak doesn't have a lot of
undefined behavior.
So, even incorrect ranges are defined to have a behavior.
But anyway, so, and the thing is, we don't even have to express all the properties of our data
as part of our type definition.
If you have your typical e-sballied data function or ballied data functions,
you can just pop them into your definition to your predicates.
You don't even have to rewrite your code.
Just pop them in, pop them in, and that's it.
Also, liquid types in A-Dak are known as type contracts.
In other languages, they are also known as that, just letting you know.
I know what you're thinking.
A-Dak, this is useful for academics, and that's why liquid types are used by academics.
Just look at your examples, even numbers, prime numbers, our cryptographers.
This is useless for real-world programming, because real-world programmers do other stuff.
Well, let's take a look at this.
Imagine we have a data structure, and we are tracking some temperature.
It could be some logging system of your server.
It could be a financial institution, tracking some stock prices.
And we have a timeframe, for example, days.
It could be milliseconds.
It could be your, I don't know, measuring some electricity in your outlet, every hour, or whatever.
And we have a high value current value and low value.
We always want to keep track of current state and the bounce of our data.
And somewhere in the code, maybe written by us or by someone else,
we just want to update the current value.
And we do serve, no, this is the very typical thing.
We are just doing an assignment.
Oh, no, we just introduced a bug.
Can you tell?
Just doing an assignment and created a data corruption bug,
because we forgot to update our values.
What if the temperature we're measuring in our garden?
The current temperature is, I don't know, 30.
And we didn't update the high value from before, which was maybe 28.
Does it make sense to have a data structure whose high value is 28?
The current value is 30.
And the lower value is, I don't know, 25.
No, we just corrupt our data structure.
Very simply, just by doing a simple assignment.
And here's the thing.
If we know the properties of our data, the high value has to always be high.
The current higher than the current value.
And the current value has to always be greater or equal to the lower value.
Why don't we write that down?
That's just a liquid type.
We express the nature of our data, how our data behaves,
or is related to each other.
We just write it down.
And it's not a common.
This is actual code.
And if you compile a data with assertions,
you will get a runtime error once you return the data.
It's a data allows intermediate incorrect data states.
In a spot, you are not allowed to do that.
And you will get a proof error if you write this code.
What about sorting algorithms?
Or, sorry, searching algorithms that are very efficient.
And they need to work on sorted data.
How can we represent that?
In most programming languages, you just cannot.
You just pass a generic array and you hope it's sorted.
In good programming, you create a new type that's sorted.
And it's only returned by procedures that use sorted data.
But we can do better.
We can express the nature of sorted data directly
as the type definition with a liquid type.
We introduce the logic of what it means to be sorted
as part of the type definition.
That's wonderful.
That's very powerful.
And I want to address one big comment that I now
I'm going to get in the questions and answers.
A for another, you're example with data, with the temperature.
Yeah, that's has been solved since like the 80s,
by using the get-in-setter pattern, object-oriented.
If your data has some kind of behavior,
you just make it private.
You don't let people modify it.
And you create a function that does the correct
modification to your data.
Liquid types are nothing-border.
But here's the thing.
Yes, you would be right.
And this example would indeed give you
better code reviews, actually.
But here's the thing.
For example, in this case, object-oriented programming,
which is how most people would do that today,
it's a whole new programming paradigm,
and liquid types are yours types that have been enhanced.
It has a high-sad data, which basically
nukes the three things you do with data, read, write, and modify.
You just basically destroyed the nature of data.
And it requires you to create an API.
So now the problem of adding data, it's on you.
And here's the thing.
Is that said, a function blocking?
Is it writing to a file?
That's forbidden in a lot of cases for hyper-performance computing.
Did you know that?
Oh, did the person that called the set-up function knew that?
Was that documented?
If it wasn't, you have got a bunch of other issues,
because normally the APIs are opaque.
People don't look how they are implemented.
And that's a problem.
Liquid types are your types.
Powerful types, but these types.
They are wonderful for instrumenting and debugging your code.
I actually can tell you that I enjoy debugging data code,
which doesn't happen with any other language.
And they will allow us to do formal verification,
as I will explain later.
And here's the thing, the wonderful thing about liquid types.
They can just go access with the rest of other programming paradigms.
If you do OP functional, they just refer to data.
So anything that works with data, all programming paradigms,
basically, they can just use it.
They are not in compatible.
And if in case you don't like this example,
you can use the limited key work, whatever.
It is a great language.
So let's go directly into functional contracts.
And I'm going to be much faster here,
because here's the thing, what are the programs?
Perums are things that take some inputs.
They process those inputs, and they generate some outputs.
It can be a simple function.
It can be whole program, whatever.
And we've been talking about data, about liquid types,
about being declarative, about explaining what our data actually is.
So we've been focusing on the inputs and the outputs,
and about their properties.
And here's the thing.
Someone could ask the very simple question.
Hey, could we apply the same principles,
but instead of just the data, the actual execution of our program?
Can we do that?
Can we add contracts to our code?
Dipes to our code, just like we do with types?
And yes, there is.
Yes, that's functional contracts.
So let's go directly to a general example.
Imagine we have a stack package where we can push data in,
and we can pop data out.
Well, we all mostly know that that is the end years.
What happens if you push too much data into stack?
Well, you just go to the buffer overflow.
What happens if you pop too much data into a stack?
Well, underflow.
How do we know what's the behavior of our functions when that happens?
If that happens at all?
Is it going to be suspended?
Well, we would need to look into the functions,
and see if it's guarded or not, or what they are doing.
Simple, if we are very worried about our users,
mistreating our functions or our data structures,
we can do explicit guarding.
And if someone tries to push too much data,
we can say, hey, sorry, you cannot do that.
And raise an exception through an exception.
And in that would be the case of failure.
But can we do better?
Would it be correct to push more data than what's available?
No, so why don't we say that as part of our function declaration?
And we do that with functional contracts.
So for example, in the push function, we say,
with, once again, that key word of header,
pre, and pre is a short form of pre-condition.
Before you are allowed to call this function,
this stack must not be full.
You are not allowed to call this function if this stack is full.
Now we don't no longer have to do explicit checking our function.
That's guarded by the pre-condition.
By all the properties that have to be true
before the function gets executed.
And we also have post-conditions.
What happens after the function has been called, in the case of the push function,
well, the size of this stack must increase.
By one, we must have added some data to our data structure.
That seems obvious that we don't even know how complex this function is
or what it is doing in between.
It could be a three-line code, a code bit,
or it could be 5,000 lines of code.
The monologics, the monolog, function of the G lip C.
It's about 5,000 lines of code.
Did you know that?
It started with this allocating some EC memory?
No, no, no.
These things can become extremely complex.
And we don't care how complex they are.
These properties are going to hold a regardless of what you do.
And we can annotate our code to do that.
Also, if you would like to see the full answer,
to how to correctly program and stack,
you go to this repository to the platinum reusable stack,
it's going to be a lot more than what you think.
There is a lot of implicit behavior that people think
and that needs to be guarded against.
And I'm here just showing you pre-conditions post-conditions.
But real world examples, they are complex.
Like global state contracts, like data dependency contracts,
et cetera, et cetera, et cetera.
This is a real piece of example.
What happens when we move some vectors or some data
to another place to another vector?
Well, these are all the things that need to hold.
What happens when we do an insertion of one bit of data into a vector?
You think that's simple?
No.
These code, by the way, is part of a Spark formal containers.
A Sparkleet is a formally verified library that you can just use.
It's under Apache version 2.
It's created by the people that dissect the critical systems.
These things are robust.
They are not only memory saved, they have no runtime exceptions.
They know runtime issues, they're correct handling
of the exceptions, everything.
And talking about safety critical systems and things like that.
Wouldn't it be great if when we program
something, we could know that it works as we expect it?
Wouldn't it be great if when we program something that we know that's doing what we hope to do?
And that our clients can be sure that our program does what they want us to do?
Wouldn't that be great even before we compile it?
Like in Rust, like for example, the borrowed sugar will make sure that your program
doesn't have any memory issues before it compiles it,
because thanks to the borrowed sugar.
Can we do all the checks before we compile that?
Well, yes, but there are a lot of checks that we need to run.
Like memory errors, program flow errors, unexpected arithmetic errors.
There is a lot that people just simply forget about.
And we can we prove that?
Oh, proof. Provers. Yes. Provers are basically compilers, but instead of creating a assembly,
they do all the checks I mentioned before, and they give you a thumbs up or a thumbs up,
and they tell you whether your program has issues.
And those issues are can be very varied, okay.
Rust World Checker is for example, a Prover for correct memory management.
And some other Provers are better wars at some different things.
For example, TLA plus, I've seen it.
We've been used more for like concurrency issues and things like that to detect those.
And some Provers are interactive and they can walk you through like your program and see if your
program has some issues somewhere.
Other Provers like Spark, which is the formal subset of Ada, which no longer is that much of a subset,
will do so automatically. You just create your code, press bottom, go and grab a coffee,
and the Prover will tell you, hey, you have an overflow here that you hadn't thought about.
It's wonderful.
And the way these things work is that they have some Provers.
The Provers have some like Perms known as SMT, Theorem Provers and things like that,
like set three, Alter, I go CVC5, that they will get your code, they will analyze it,
and they will tell you where what could go wrong and things like that.
So do people actually use this in the real world?
Most people think of oh yes, like cryptography people.
But real world parameters don't need these techniques.
The answer is yes, people are working in an operating systems.
When you need a reliable operating system that's just not going to break, you use these techniques.
Liquid types, contracts, formal proofs.
Of course, yes, cryptography.
And one of the beautiful things about Ada, you can just work on it on embedded systems.
A lot of other Provers don't do that.
And a lot of people are worried about performance.
I would recommend you click on the optimized for performance link there.
The guide that created this cryptographic library,
optimized it for performance while maintaining full proof correctness.
But not only that, we use a ton of software daily that we are just not aware of,
that we just expect to work.
Are we sure it's just going to work?
Our Perms constantly parsed JSON or XML.
Are they going to work?
How many times have we seen security issues every time someone gives a model,
form thing, a model form, jpeg or whatever?
Quite okay, image format.
Someone who we actually have here created a library,
it's formally verified to work on it.
And it doesn't matter if you feel it incorrect data,
an incorrect, malformed image.
It's just not going to break.
It has been verified to do that level.
So, as a conclusion, liquid types and contracts allow us to express
the properties of the nature of our code and our data,
and they document and give meaning to our program at the code level.
They serve us instrumentation, the bug ability of our code,
and they allow us create very robust code and for proofs.
And the formal proofers, the formal verification of our code,
gives us the assurance that things are going to work as we expect them.
They are going to be memory correct, they are going to have no exceptions.
Or if they have exceptions, they are going to be handled correctly
that we are not going to have overflows underflows
incorrect data management, et cetera.
And they are wonderful.
And especially Spark is a wonderful teacher because it has a counter example,
flag that you can pass it and it will explain you
and walk you through how you got something wrong, which is wonderful.
So, and just a bit about Ada, the reason I love Ada
is because it has all this features I have mentioned,
but you can also work on embedded systems we feel without operating systems.
And Ada supports a ton of architectures,
it's low level, high level, it's very readable,
you can interrupt with C code, it's wonderful.
Yes, it's not perfect, some issues are part of the community
and the ecosystems, some limitations are part of the language by design
in order to get these robustness.
But thank you, and other questions how much time we have for those?
One minute for questions, oh, sorry about that, thank you.
So one quick question only, yes?
When you use these steps, you said,
to what degree are they verified at a compound time versus a runtime?
Oh, so, thank you, I mentioned that with Ada,
we have the beautiful thing of being able to,
oh, let me repeat the question for the online people,
what are the advantages on the differences of runtime
and a proof time of being able to select those, no?
We are the ones by versus a compound line.
Well, are the difference.
So, at runtime, in Ada, you can select
if you just write your program, you can select full runtime correctness
with that, it comes to a course of the runtime.
And Ada is a little bit lenient in some of the features.
You can do a runtime like temporary, you can have temporary incorrect
to state if you so wish.
In Proof, Proofers are very strict.
They will not allow you to have any intermediate incorrect data
or state, and the runtime comes with the cost
of, well, they actual checks,
where they can not place a runtime.
The size of the objects of the program is going to be larger,
but you gain the bug ability and the traceability
of your programs, that's why it's so we sit to the bug Ada.
You just run it, run it on another bug,
you just tell it to catch all assertions, to catch all exceptions,
and you just close your eyes and let the bug refine it.
But the proofer, it will be a bit slower, noticeably slower.
But once it's been proven, you can just
trust the compilation of your code and go ahead with it
and trust me it fully.
So there are no more time because we have an issue.
Nonetheless, go ahead and write it to me in my email if you
also want.
And I, reminder, yes, Ada allows you to do very low level
control of data.
So thank you.
APPLAUSE