I know my title is a little bit contentious maybe, but I'm a rest developer, I'm allowed
to say that.
So, who am I?
I'm Alia Bequet.
I'm a rest-competitive developer, I've been now for 10 years.
I came to us actually because of Ada.
Before that, I was doing Ada.
Well, I've been doing rest for 10 years now, and my Ada's a little bit rusty, so it's very
interesting.
But I still coded if you know, and then, anyway, it's talk is not about rest-of-engellism.
It's the out-of-way around, more.
It's just showing where we're currently at, because we've been doing a lot of work on getting
rest ready to use and take the grid of systems more, and yeah, so what have we been doing
here?
A bunch of topics.
The unsafe keyword is to think that, basically, what in Ada is the by convention unchecked
keyword.
It's not really a keyword in Ada, but it's what you used to say, like, this thing is probably
going to be dangerous.
You should read a documentation otherwise, if you think it's going to blow up.
We use have some problems there in rest.
I think we've gotten through all of them now, so I'm going to check, give this small
intro there, generic packages, modules, really cool in Ada, rest, yeah, crickets, safety
certification, going to go into details there, and we have contracts now.
They're coming, they're not merged yet, fun, but PR's open and almost ready to be merged.
And it's up-type.
That's kind of my baby that I've been working on for like, whatever, 10 years, and we've
gotten there, and so I'm going to most of the talk is going to be about sub-typeing.
So, uncheck first, unsafe.
This is an example of code that you can write in rest up to a few months ago, that would
have been totally fine, compiling, and your program would have blown up, because you created
a malloc function, and malloc is a weak symbol in most code that you have out there.
So if you just define a random malloc function with a literal symbol name malloc, you are
now the owner of the malloc function, whatever you write in there is malloc, and so if you
just do something like random integer, well, your code is probably going to blow up because
somebody is going to call malloc and dereference it, and well, that's something to happen.
Anyway, we fixed that you now have to actually specify unsafe somewhere in there before
you didn't have to, and I'm blowing up a program without writing unsafe.
Yeah, no, not good.
So we fixed that.
Generic packages and modules.
If you write a generic package and rest, you get this error message, like it's so unsupported,
even the diagnostics, no, no, what you're talking about, and rest is actually famous for having
good diagnostics, so anyway, I'm going to fix that soon, but just fixing the diagnostics,
not actually implementing any feature.
Safety certification, we are safety certified, we have a application of, not for, well, yeah,
fair seen.
Fair seen is used in safety code systems, you're allowed to actually use your stuff
in, like, cars and whatnot, at least in Germany now, I don't know about other countries.
And there were some little bit of drama, like, this was used to be an interoperable
with ADACORE and fair systems.
It is now not drama happened, people quit stuff like happen, I don't know if people quit
because of this, but anyway, cool, we have this now, and it's being distilled, being developed
for extended, and it's always up to date with, like, the current rest version, maybe,
like, six weeks behind or something, but yeah.
So, contract, contract and rest are similar to contracts before, like, ADAC, what's it 2012.
When we did, we can contract actually in a language.
It's basically attributes, which are more similar to how you have random comments somewhere,
except that the language will actually now check these attributes, and you can specify
arbitrary pre and post conditions.
They're not actually formally checked in the way that a spark checks them, but we have
to Connie formal checker for rest, which is similar to spark, it has all this S&T solvers
in there, it gives you diagnostics, it creates counter-examples and whatnot.
It's not fully complete yet, but it works for a lot of rest code, and it's being used
to, like, prove small, cut rest code as completely free of runtime exceptions.
So, that's cool.
And, well, the thing I want to actually want to talk to you all about, after giving you
this small update, pattern types.
Pattern types in rest are similar to ADAC, except what we normally have in rest is just
like concrete types for, like, a non-zero U32 that's like an actual type in standard library.
You don't specify, like, I just want my integer to not have zero.
What you do is you use this building type, and you actually define this type yourself.
You can't do a non-ten U32, that just doesn't exist in rest yet.
And, similar for pointers, there's a non-nal generic type that you can define for any kind
of pointer type, and it will give you a non-nal pointer, but this is just a standard
library type.
It has a lot of magic in there to make it work, but it's not something you as a user
will actually be defining yourself.
It's kind of side, so the rest of the stuff is actually well explainable.
In rest, types, type aliases are not strong.
Not like ADAC where you have, like, a concrete different type, rest, the left side and
the right side, even though they are called different things, they're specified the
different lines of code and whatever, they're just the same type.
Like, rest will not actually know that bar exists.
It will just know that, like, there's a U32 here now.
It's not a pre-processor, but it will just transparently make this disappear.
It's just a help for you to not write the code twice and be able to easily change
like type definitions.
So, that keep that in mind when I'm going into my examples that are following patterns.
Noterside, before we go into actual pattern types, patterns in rest are similar to the
whole case patterns that you have in ADAC.
You can match on something and then, like, this is almost the same syntax.
The rest formative just doesn't put spaces between the dots, otherwise, it's pretty much
the same thing.
And there's other syntaxes, like, the ore pattern, which is, like, do separate things.
Like, this is a cat dog or bat, and then if it's one of these, then you go into
dot arm when others go into the rest.
These kind of patterns are what we actually want to use for specifying subtypes and rest,
because we already have to concept of something, matches, some specific subsection of that type,
and we just want to reuse that because we don't want to duplicate another system.
So, that's what we're basically trying.
One cool thing about rest, you can specify patterns that are matched together.
So, here, I'm matching on two variables at the same time, and it's required to the first variable
is in range one to ten, and second variable is dot or cat.
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.
So, you can combine multiple types and check them at the same time together.
And that's something that we want to use in our pattern types too.
This also works in data, but you need to specify more complex bounds there.
It's not like a building thing directly.
You need to do these front-hand checks as far as I can tell.
So, how would this look?
We had the earlier example of non-zero, and now my plan for the very far future is that the standard
library will actually replace the non-zero U32 type with this type of alias.
It will literally be a U32 is one dot dot, so a U32 that starts at one and can be any value after that.
And similar thing for null pointers, we don't use the not key word because we are less
using such rules and short of stuff, so we do not bang, and then no.
This syntax might completely change, depends on what the language team decides, but
something like that will happen.
And so, we can define those types that are really building into the standard library.
So, what else can we do?
First, I already mentioned that pattern types do not do strong typing, so you do not get
separate types. If you do the same type definition twice, it will be exactly the same thing.
If you say U32 is one dot dot something, another person defining in a completely different
library completely somewhere else, same thing, same type.
And for the language knows about you, pattern types are not actually doing sub-type
pattern types, only curves between each other, like the compiler will insert conversions,
but there will be no actual type system sub-type in where the types are actually like
sub-type stuff each other like what happens with lifetimes and rust.
Lifetimes do a lot of sub-type thing, but we are trying to keep it to lifetimes and not
to explode that more. That might change in a future, but for now we are trying to get it.
So, how do you actually create a pattern type? Up to this week, earlier this week, what you
have to use was a transmute, like unsafe code to convert an integer to the actual sub-type.
And now, what you can do is you can just specify literal, just like an eight-hour,
you specify literal, and assign it to your sub-type. And the compiler will just check,
this is literally actually in range for that sub-type, and if it's evidence and it will
just merge it, and if it's not, then it will actually emit an error. On the other hand,
if you're converting a variable, so you declare a variable here, and you convert that,
you need to currently use transmute, there's no good conversion in eight-hour, you literally just
use the type, and it will do a run-type check for you. But we're working on that, and what we
want to do is, thanks for the previous presentation, I stole your stuff. Here's a great type,
which is 1 to 6, and a passing grade, which is 1 to 5, German passing grades, anyway.
And you have a variable of type grade, however you get that value. What you then want to do is,
do you convert that grade with tri-from into a passing type, and then you get an option back,
because either the conversion succeeds, then you get the thing in your option sum, or it doesn't
see getting into a non-new, don't actually get the value. If it doesn't succeed, you don't get
a value. Important stuff, good that ADA and Rust are getting this right in contrast to other languages.
And there's lots of more stuff that I want to do. These things don't work yet at all, but
Rust patterns. I want to basically, if you can write a pattern in Rust, in like a match,
I want you to be able to write a pattern type for it. So having combinations of like a type where
the U32 must be between 1, 0 and 100, and the string must be limited to specific things. And
this is in combination. You cannot go out of this, these belong together, and maybe even at some
point have constraints where like 0 to 50 means cake and 50 to 100 means fruit or something like
that, where you can make more complex combinations of that. I want to, if you can specify the pattern,
I want you to be able to write a pattern type, and we have a good plan for forgetting there.
So, I'm almost out of time, so let's go to the summary.
Genetic modules completely to do not happen any time soon, don't wait for it.
Contracts are working progress, they're happening pretty fast, and I think they are already supported
in the county model checkers, so we'll just get them basically for free as a static check.
Head and type, I'm working on them. If you want stuff, complain to me. I'll try to make
stuff work. My next step is idiomatic conversion, so to try from that you saw earlier,
and where we've cut up, we have safety certification, and we're some, by default, pretty much
module loads, some, something that's back said we're fixing, but like, that's a compiler back,
not an actual language bug. Thanks, questions.
APPLAUSE
So, the matching on, let's write a constraint,
induce certain strings, kind of scares me. Why can't we just have the,
like, having it in just the generic types that implement the rate, and like, if, like,
the rate for me, probably, that you're a library, or whatever, because, ideally,
whenever I see, it can be these strings, it gives me, maybe, like, helps for clients.
OK, the question is, why can we actually match some strings,
and say, like, this could be like cake or fruit or something, and what, why isn't there,
like, some better system, I think? Yeah, I don't actually know it's a hard topic to do something
better, they're really like, you can do runtime checks, similar to, to the ADA runtime checks,
or you can do this oralist thing. We don't really have a better concept. Like, there's ideas
for integrating, like, RECX into, like, matches or something like that, but it was, like,
very far off, and I don't know if we're going to do that or anything at all.
There might be better ways to do this. I don't really know about it. I'm happy to talk about
ideas, but, yeah, I don't know.
Considering that you feel that Rust has caused out in terms of safety certification,
my question is, how in Rust do you prove the absence of runtime checks?
The question is, how do you prove in Rust, the absence of runtime exceptions? Well, similar to
all, we have Spark and Ada, we have Connie and Rust. It is a working progress, but it does
actually do the same kind of checking, and it is actually being used for pretty much the same
things. With one minute, it's a one more question.
Thank these subtitles. Will I be able to explain Spectre's subtitle in a country, like,
first reference, that I also have the, what's the, what's the generic type? Will I be able to
pass into subtitle? Will this have any problems? Or, uh, because I'll feel like that you get this
subtitle. Can you? Can you? I assume I've got a subtitle. Yeah.
Raise one to five, and I expect that you said two, but I'd be able to pass it on to the subtitle.
Okay, the question is, if you have a subtitle, can you use that anywhere where you can use the
normal base type of that? And the answer is, you can outside of generic context first, because
there's implicit conversion from subtitles to the base type, because every subtitle is a valid
version value of the base type. But, um, if you're using generic context, um, we're currently
figuring out how to implement traits for subtitles, um, and, and how to implement, like, implicit
conversions there. Um, we're not using actual subtitle, so we need to figure out something better,
uh, but it might be that the answer is all this. We actually need full on subtitle, uh, we don't
know yet. I have a couple of minutes. Cool. More questions. Over there.
The question is, uh, how do you specify, uh, to some mentally equal, but, uh, with different,
uh, representation, like, to two types was the same representation, uh, for the, for the,
use and language by the different layout representation, and, uh, I don't actually think you can do that.
The question is, uh, can you use constant functions and contracts? Right now you can just use any
runtime code, uh, because they just run time checks, um, contracts are working progress, and we're
figuring out the details there, but the simplest thing was to simply make them just run time checks
and to start in the end of function of the function right now, and we'll figure out the details as we go.
Yeah. So the question is, why is this in text highlighted, not actually catching, there's,
uh, pre-conditions and post-conditions in the, in the, in the contracts. And, uh, the thing is the
contracts are attributes, and attributes don't actually support expressions in them, and they
were some bunch of hacks going on there. Like basically the attribute is a proch macro that generates
some super secret internal rest-replication language, um, and, uh, we don't actually know where
this is going yet. It might actually end up just being surface language syntax that actually
doesn't use attributes, uh, but like this is working progress and the language team would like us
to be more using weirters syntax to start with. So today we don't prescribe what the language
is going to go and, and, and up with, and not get people used to some, something that actually
looks like they want to use it in the end.
Yeah. So the question is, um, if you, for example, use a non-zero type inside an option, what you get is,
the same size as the non-zero type, because the option knows like, oh, there's a zero missing,
I can just use that for my non-value. And, um, uh, the pattern types actually, that's the first thing
I implemented before. I implemented anything else in pattern types, implemented if you do like
zero to 100, all the other possible values of your integer are now for three for other
enums to take, to put their, uh, discriminants in. So you can actually nest like 50 options inside
each other, and in the middle there's a zero to 100, and, um, that will just be the same size
as the original value.
Well, the pattern types, oh, so the question is, can you do, it's supposed to say like, which bits are supposed
to be there and which not, and the answer is simply the range that you're specifying that's
the value range and everything else is invalid. And, uh, if you specify like multiple ranges,
right now, the limitation is it will just pick the biggest space of invalid values and use that
for everything. It will not actually preserve all the invalid spaces.
That's cool. Time.
For I'm going to be in a whole way for questions if people want to back me about stuff,
uh, have you talked about rest? Talk about data and stuff. Um, grab me.