►
Description
No description was provided for this meeting.
If this is YOUR meeting, an easy way to fix this is to add a description to your video, wherever mtngs.io found it (probably YouTube).
A
Mic
Check
great
hi
all,
and
thank
you
very
much
for
sticking
around
with
me
until
the
bitter
end.
So
yes,
as
neil
already
said,
let's
talk
about
rust.
Rust
is
a
very
recent
programming
language
designed
by
Mozilla
and
it's
kind
of
claimed
to
be
a
safe
and
modern
systems,
programming
language.
So
let
me
explain
some
of
these
buzzwords
here.
It's
a
modern
language
in
the
center
that
comes
with
all
the
features
that
we
all
love
from:
our
nice
and
high-level
functional
languages.
A
First-Class
functions
like
closures,
algebraic
data
types
polymorphism
and
traits
which
are
rusts
type,
a
take
on
type
classes
and
associated
types.
At
the
same
time,
it's
it's
kind
of
a
low-level
language
as
well,
because
it
gives
you
control
over
resource
management
in
particular
memory
management.
So
in
rust
you
have
control
over
when
memory
is
allocated
and
D
allocated.
There
is
no
mandatory
garbage
collection
and
you
also
have
control
over
how
data
is
layered
or
the
memory
where
they
are
pointer
and
directions,
and
things
like
that
and
rust
chips.
A
All
of
this
together
in
a
package
with
a
strong
type
system
that
guarantees
or
is
claimed
to
guarantee
memory
safety,
as
well
as
threat
safety.
So
in
the
Rust
Belt
research
project
we
are
well.
Essentially
we
have
the
goal
of
verifying
these
claims
on
a
mathematical
basis.
So
in
in
this
paper,
we
report
on
our
progress.
So
far,
concretely
are
the
contributions
represent
here.
Are
we
design
we
defined
a
lambda
rust,
which
is
a
core
calculus
representing
a
fragment
of
the
rough
programming
language
and
it's
type
system?
A
We
have
improving
semantic
soundness
of
lambda
rust
by
giving
it
a
lot
circulation
in
iris,
which
gives
us
not
just
the
types
on
as
result,
but
also
a
way
to
reason
about
unsafe
code,
and
then
we've
applied
this
and
reason
about
reasoned
about
a
bunch
of
the
interesting
and
important
unsafe
code
that
comes
in
roster
library.
So,
before
I
go
into
these
contributions,
however,
I
will
teach
you
a
little
rusty
if
I
only
had
one
slide
to
explain
the
type
system
to
you,
it
would
be
this
one.
A
The
central
proposition
of
the
rest
type
system
is
to
rule
out
the
unrestricted
combination
of
aliasing
and
mutation
and
the
mechanism
through
which
rust
rust
achieves.
This
is
ownership.
So,
for
example,
if
you
create
a
vector
influence
and
data,
and
then
you
call
a
function
which
could
be
called,
send
and
pass
the
vector
to
that
function,
rust
consider
this
to
be
ownership
transfer,
so
you
owned
the
vector
after
you
created
it,
meaning
you
are
the
only
exclusive
person
able
to
access
it
and
you
gave
it
to
send
and
now
it's
theirs
and
no
longer
yours.
A
One
consequence
of
that
is,
if
you
try
to
you,
do
anything
to
the
vector
again
later.
Actually
rust
will
disallow
that
it
will
tell
you
that
V
has
been
moved,
and
this
is
actually
really
useful,
because
one
of
the
things
sent
could
do
is
it
could
spawn
a
new
thread
and
put
the
vector
there
and
have
the
thread
loop,
computation
on
the
side,
even
after
Sanders
returned
and
then
there
would
be
data
raised
here,
and
that
would
not
be
fun.
A
So
in
general,
if
you
have
some
variable
X
of
type
T
rust,
consider
this
data
to
be
owned
at
the
given
type
ownership
implies
that
you
can't
do
mutation
and
hence
no
aliasing,
and
you
can
even
deallocate,
because
really,
if
you
own
this,
nobody
else
even
knows
the
data
or
even
exists.
However,
ownership
can't
be
everything,
because
if
you
look
at
this
example
a
closely,
you
can
see
that
we
actually
called
a
method
here
on
the
vector
V
and
we
were
allowed
to
use
it
again.
So,
what's
going
on?
A
Well,
let's
disregard
this
method
call,
and
then
we
can
see
that
what
actually
happens
here
is
that
we
are
creating
a
reference
to
the
vector
and
passing
that
reference
to
push.
So
the
crucial
difference
here
is
that
send
is
passed
by
a
value
which
and
rust
is
interpreted
to
be
ownership
transfer
where,
as
push
is
passed
by
a
reference,
and
in
this
case
push
is
said
to
borrow
ownership
of
the
vector
temporarily
well,
I
said
temporarily,
but
I
should
really
make
this
precise,
because
we
don't
want
to
just
be
guessing
here.
A
How
long
is
temporarily
well
to
control
this
rust
uses
the
concept
of
a
lifetime,
which
is
also
called
a
region
in
the
literature,
so
in
the
full
type
of
push
you
can
see?
Tick
a
here
is
at
the
lifetime
of
the
reference
which
pushed
X's
argument
and
it's
an
angle
bracket
indicating
that
the
function
is
actually
pulling
off
again.
A
That
can't
we
left
hand
you
think
there
is
no
lifetime
given
in
the
source
code,
above
so
the
compiler
and
first
the
left
hand
for-
and
this
scare
didn't
further
Lefton
to
be
just
the
duration
of
the
function
call
which
then
explains
why,
after
function
returned,
we
can
actually
call
send
and
use
the
vector
V
again,
because
push
can
no
longer
be
using
it.
The
borough
has
expired,
so
ampersand
mutex
is
a
way
to
create
a
mutable
reference
to
some
data.
A
Implicitly
there's
a
lifetime
here,
which
is
inferred
by
the
compiler
mutable
references,
do
a
lot
of
mutation
and
hence
not
allow
any
aliasing,
so
mutable
references
are
always
unique
pointers.
Now
we've
seen
two
examples
of
I'm
having
mutation
and
no
aliasing
so
unsurprisingly,
the
third
example
involves
aliasing.
A
So
concretely,
this
code
creates
a
local
variable,
then
spawns
to
threat
that
both
concurrently
read
a
pointer,
pointing
to
the
stack
frame
of
the
main
thread
printing,
the
current
value
of
that
of
that
variable,
and
then,
when
both
threads
are
done,
we
mutate
X,
what's
going
on
here
is
that
ampersand
X
is
a
way
to
create
a
shared
reference
with
which,
like
mutable
references,
come
with
a
lifetime
that
is
inferred
by
the
compiler
and
shared
references.
As
the
name
indicates,
they
can
be
a
Lea.
A
They
can
be
shared
by
multiple
threads
in
this
case,
and
hence
they
do
not
allow
rotation.
We
can
also
see
that
in
this
case,
the
lifetime
inferred
by
the
compiler
is
actually
the
duration
of
this
joint
function.
Call
which
means
that
once
join
is
done
and
both
threads
are
actually
done
computing.
We
can
mutate.
The
variable
again
so
share
references
having
a
lifetime
means
that
we
can
temporarily
make
data
read-only
and
shared
and
then
later
regain
full
exclusive
access.
A
So,
to
summarize,
what
we've
seen
so
far
rust
type
system
is
based
on
ownership,
which
comes
in
three
flavors,
there's
full
ownership.
You
can
do
anything.
You
want
and
then
there's
two
kind
of
temporarily
borrowing
ownership
which
comes
in
the
flavors
of
mutable
and
aliasing,
and
both
of
these
are
controlled
by
lifetimes.
So
this
is
all
working
very
nicely.
The
problem
now
is,
this
seems
pretty
restrictive
right.
Sometimes
you
do
need
alias
mutable
state,
maybe
you're
doing
shared
memory
concurrency
and
you
have
locks
or
something
like
that.
A
Maybe
you
prefer
a
message
passing
and
you
have
some
channels
that
sin
theta
between
threads
there's
also
shared
mutable
state
there,
or
maybe
it's
sequential
setting
and
you're
doing
reference
counting
for
your
memory
management.
So
what
is
rusts
answer
to
this
problem?
Well,
let
us
look
at
an
example.
A
This
program
creates
a
new
text
and
mutexes
contain
data
and
rust,
so
we
initialize
this
with
value
0,
and
then
we
spawn
two
threats
that
both
acquire
the
lock
do,
some
error,
handling
or
well
not
to
error
handing
it
nor
the
Unruh
appear
and
then
increment
the
value
that's
stored
in
the
lock
and
implicitly,
the
lock
is
then
released
again
when
this
goes
out
of
scope
and
then
once
both
of
those
words
are
done,
we
print
the
current
value
and
of
course
we
expect
this
to
be
3.
So
to
understand.
A
What's
going
on
here,
we
should
look
at
closer
at
the
type
of
this
lock
method.
First
of
all,
it's
a
polymorphic
method
again
taking
working
on
any
lifetime,
and
it
takes
a
shared
reference
to
a
mutex
as
its
argument.
It's
cooler
this
is
shared
because
the
holy
idea
of
a
lock
is
that
multiple
threads
can
be
racing
and
trying
to
access
the
lock
at
the
same
time.
So
if
we
wouldn't
allow
aliasing
here
that
wouldn't
make
any
sense,
the
return
type
is
little
unwieldy,
but
you
can
essentially
think
of
this
as
being
a
mutable
reference.
A
There's
some
more
magic
going
on
to
do
this
automatic
unlocking.
So
what
we've
seen
here
is
a
method
which
takes
a
shared
reference
and
then
gives
you
a
way
to
mutate
stuff
in
there.
This
is
a
phenomenon
that
is,
there
has
several
instances
in
this
9
library,
it's
code,
interior,
mutability
and
it
seems
to
completely
break
everything
I
said
so
far,
and
it
seems
to
be
also
inherently
unimplemented,
because
there
are
types
that
you
shouldn't.
Allow
you
to
do
anything
like
that.
A
Well,
for
the
second
part,
the
reason
that
works
is
that
rust
has
unsafe
box
and
inside
unsafe
blocks.
There's
additional
things
you
can
do
and
the
compiler
kind
of
says
you're
on
your
own
there.
So,
for
example,
you
can
call
into
the
operating
system
and
ask
P
thread
to
please
acquire
a
lock
for
you,
and
this
is
what
the
implementation
of
lock
does
if
you
run
it
on
Linux.
A
However,
the
claim
of
the
developers
of
this
library
is
that,
even
though
the
implementation
of
the
mutex
is
unsafe,
its
API
is
safe.
So
if
you
write
safe
code
that
uses
the
mutex,
you
can't
screw
up,
and
you
can't
have
data
races
or
other
kind
of
memory
problems,
and
this
is
not
isolated
to
mutex.
The
explicity
of
rust
is
continuously
extended
in
this
way,
not
just
understand
a
library,
also
by
user
libraries.
A
So
this
join
method
we've
seen
a
couple
times
is
actually
an
additional
library
that
you
can
add
into
your
rust
code,
which
has
a
sophisticate
implemented
based
on
average,
stealing,
who
are
using
some
unsafe
code
to
be
well
possible
and
also
to
be
efficient
and
again.
The
claim
of
the
author
is,
if
you
use
this
from
safe
code,
your
your
program
is
not
gonna
crash.
I
have
any
other
kind
of
memory
or
threat
safety
issues.
So
this
brings
us
back
to
the
goal
of
our
raspberry
search
project.
A
We
want
to
actually
prove
these
claims
of
the
rough
types
of
some
developers
and
of
the
library
developers
true
and
clearly,
because
of
this
extensible
nature
of
rust.
We
have
to
do
this
in
a
way
that
our
proof
is
also
extensible
and
we
can
kind
of
prove
new,
unsafe
libraries
safe
without
redoing.
The
entire
proof.
A
So
now,
in
the
second
part,
I'm
going
to
give
you
an
impression
of
what
we
did
there,
we
defined
this
lambda
rust
language
and
a
type
system
for
it.
The
type
system
comes
with
a
bunch
of
dead-end
types
like
Moonies
and
integers.
Three
kinds
of
pointers
matching
the
three
kinds
of
ownership:
that
rust
has
owned,
pointers,
new
table
and
shared
references,
some
types,
product
types
and
also,
of
course,
function,
types,
recursive
types
or
the
usual
business.
A
These
types
of
them
collected
in
the
Taiping
context,
which
assigns
types
to
pass.
That
provides
a
way
to
directly
talk
about
the
types
of
individual
fields
of
stretched,
because
the
rest
types
are
actually
tracks
these
separately.
For
the
purposes
of
these
references
and
borrowing,
and
of
course
we
have
a
cup
of
typing
judgments
which
are
a
substructure,
it
shouldn't
be
a
surprise.
After
all,
the
rest
type
system
has
ownership
and
you
can
lose
access
to
data.
A
So
we
have
a
typing
judgment
for
typing
individual
instructions
which,
as
usual
and
sub
structure
type
systems,
comes
with
a
pre
and
the
post
typing
context
indicating
which
stuff
we
have
before
and
after
executing
the
instruction-
and
there
are
some
additional
context
for
tracking
lifetimes
and
then
we
have
having
good
me
typing
judgment
for
wholly
functions
and
whole
functions
are
written
in
continuation
passing
style,
so
it
doesn't
come
with
the
post
type
in
context.
Instead,
it
comes
with
the
context
K
tracking,
the
possible
continuations.
A
So
of
course,
you
may
not
be
expecting
me
to
show
you
some
typing
rules,
so
we
do
have.
We
do
have
typing
words.
We
have
plenty
of
time.
In
fact,
you
have
so
many
interpreters
I'm
not
going
to
show
you
any
of
them
and
focus
on
the
high-level
aspects
of
the
type
system.
Instead,
the
usual
thing
we
will
do
now
is
prove
a
form
of
syntactic
type.
A
Safety
result
through
progress
and
preservation,
but
the
problem
with
this
is
we
would
not
have
a
story
for
doing
unsafe
code,
so
we
do
what
essentially,
what
direct
told
us
to
do
in
his
keynote,
and
we
use
a
semantic
approach
based
on
logical
relations.
Concretely,
we
define
an
ownership
predicate.
You
can
think
of
this
as
a
somewhat
elaborate
version
of
this
value
relation
that
Derek
had
in
his
talk
that,
for
every
type
Tao
tells
us.
What
does
it
mean
to
own
data
at
this
type?
Ownership
predicate
in
our
model
take
two
arguments.
A
A
So
we
kind
of
can
kind
of
think
of
this
as
being
all
the
adjacent
memories
that
one
after
the
other,
and
then
the
predicate
tells
you
is
this
valid
at
the
given
time
once
we
have
defined
that
for
all
types,
and
we
later
give
you
a
glimpse
for
how
we
do
that,
we
can.
Excuse
me
sorry,
so
we
and
of
course
we
define
this
predicate
and
iris
shouldn't,
be
too
surprising
and
that's
very
useful,
because
iris
kind
of
comes
the
built-in
notion
of
ownership.
So
we
don't
have
any
trouble
modeling
that
part
of
rust.
A
It's
also
useful,
because
iris
lets
us
derive
new
reasoning,
principles
inside
the
logic,
and
this
is
very
very
useful
later,
once
we've
defined
this
ownership
predicate,
we
can
lift
it
to
contexts,
and
you
can
see
already
here
that
we
are
fully
using
the
fact
that
we
are
in
a
separation
logic.
Clearly
in
Rus.
If
you
have
two
vectors
and
give
away
one
of
them,
you
want
to
know
you
still
have
the
other
vector.
A
So
we
put
a
separate
in
conjunction
between
the
elements
of
our
typing
context
and
if
we,
if
we
wouldn't
use
the
separation
logic,
would
now
have
to
start
manually
talking
about
splitting
resources.
We
don't
want
to
do
that
once
we
have
all
the
typing
contexts
defined,
we
can
define
typing
judgments
and
again
we
make
use
of
the
fact
that
iris
provides
a
program
logic.
So
we
use
a
hot
wrapper
to
say
what
is
it?
What
is
it?
What
does
it
mean
to
be
a
well
typed
instruction?
A
We
are
the
pre
and
post
type
in
context,
become
pre
and
post
conditions
of
the
hot
river.
So
next
we
have
to
show
that
our
semantic
triples
have
anything
to
do
with
the
syntactic
type
system
we
defined
previously.
So
I'm
here
are
two
all
the
typing
rules.
I
didn't
show
you
and
the
exact
rules
don't
matter.
A
The
important
thing
is:
there's
a
bunch
of
turn
starts
near
single
turn
starts
and
what
we
now
do
is
we
replace
them
by
double
turn
starts,
and
this
makes
it
a
statement
in
iris
and
for
every
single
proof
rule
we
go
ahead
and
prove
this
iris.
This
iris
statement
at
the
theorem,
once
we
did
all
that
we
get
as
the
corollary
that
well
type
programs,
can
go
wrong,
so
there's
no
later
races
and
there's
no
invalid
memory
axis.
However,
we
actually
get
much
more
than
that.
A
Mutexes
loses
uses,
features
which
we
won't
get
a
safe
type
system
for,
however,
we
can
manually
prove
that
mutex
is
semantically
well
typed
at
the
type
that
is
given
in
its
in
its
API
and
because
we
have
shown
that
everything
that
happened,
that
we
have
shown
this
compatibility
lemmas
for
everything
that's
happening.
We
can
actually
lift
the
semantic
softness
of
mutex
and
link
it
with
the
syntactically
type
checked
code
and
obtain
semantic
soundness
of
the
entire
program.
A
So,
in
the
other
words,
the
whole
program
is
safe
if
the
unsaved
pieces
are
safe,
and
this
is
where
the
semantic
approach
really
gives
us
a
much
stronger
result
than
just
showing
a
syntactic
typed
exterior.
So
in
the
last
part
of
the
talk,
I
want
to
give
you
a
brief
impression
of
how
this
type
ownership
predicate
looks
like.
So,
let's
have
a
look
at
owned
pointers
to
some
type
tau,
there's
a
bunch
of
bookkeeping
going
on
here,
because
we
have
these
lists.
But
what
does
me
that?
A
What
it
says
that
its
core
is
hopefully
the
kind
of
the
interpreter?
You
would
expect
there's
a
maps
to
there
saying
we
own
some
memory.
We
have
some
location,
L,
there's
a
list
of
values,
W
and
this
list
of
values
is
a
valid
towel,
whatever
the
contour
points
to
right
now.
The
really
interesting
types,
of
course,
are
the
ones
which
makes
which
make
was
kind
of
different.
A
There
are
these
reference
types
that
come
with
a
lifetime
all
right,
so
first
of
all,
I
would
like
to
point
out
how
the
mutable
reference
is
pretty
similar
to
the
old
pointer.
It
also
has
this
maps
to
some
list
of
values
and
then
there's
the
list
of
values
as
valid
as
how.
Well
then
there
is
this
funny
thing
here,
which
is
this
looks
like
a
tie,
but
it's
actually
a
connective
in
the
logic.
It's
like
a
modality.
A
This
is
really
find
a
way
to
be
able
to
talk
about
borrowing
in
separation
logic
in
general,
not
just
syntactically
as
part
of
the
type
system,
and
we
call
this
the
lifetime
logic.
The
central
proposition
of
the
tab
lifetime
logic
is
that,
in
contrast
to
traditional
separation
logic,
where
you
split
ownership
in
space
right,
P,
star,
Q
means
P
and
Q
hold
for
different
parts
of
the
heap
and
the
left-hand
object.
We
can
separate
ownership
in
time.
A
So
let
me
demonstrate
this
by
looking
a
little
closer
at
the
central
approval
of
the
lifetime
logic
at
the
bottom.
You
can
find
a
timeline
where
now
is
the
point
in
time
when,
when
the
rule
is
applied
and
dagger
Kappa
is
the
point
in
time
at
the
left
and
gets
killed
and
in
so
before
they
got
kept,
are
kept
as
alive
after
they
got
Kappa
dead.
Now
this
rule
says
that
if
we
own
any
assertion
P,
then
we
can
do
the
following.
We
can
split
P
into
two
parts.
A
The
first
part
grants
us
access
to
P
Y
the
lifetime
cap,
our
last
that's
from
now
until
take
a
Kappa,
and
the
second
part
grants
us
access
to
P
when
after
Kappa
has
ended.
So
that's
that's
essentially
from
daga
Kappa
until
the
end
of
time,
and
because
these
two,
these
two
parts
of
the
timeline,
are
disjoint.
It
is
justified
to
put
a
separate
in
conjunction
between
these
two
pieces,
even
though
they
both
take
talked
about
the
same
resources
P
and
the
way
we've
shown
that
this
makes
any
sense
is.
A
So
this
brings
me
especially
to
the
end
of
my
talk,
the
in
the
paper.
We
show
a
couple
more
details
about
lambda
rust,
the
language
about
the
type
system,
some
of
the
typing
boots
that
didn't
show
you
and,
of
course
the
left
hand,
logic
and
a
whole
bunch
of
rules
for
that
we
also
show
how
we
can
handle
in
theory.
Immutability.
Remember
that's
this
idea
where
you
can
actually
in
controlled
ways.
A
Mutate
share
data
I
hope
it's
somewhat
intuitively
clear
that
this
makes
the
the
justification
for
why
share
references,
work
more
complicated,
but
it's
not
just
shared
references
are
read
only
in
a
mutex.
You
can
actually
write
to
them,
so
the
justification
can
become
more
complicated.
We
explain
how
that
works
and
for
two
country,
two
types:
a
few
tags
and
cell.
A
Moreover,
we
have
a
compromise
ation,
where
we've
shown
a
couple
more
types
to
be
that
also
all
in
work
interior
mutability
to
be
semantically
well
typed,
and
in
one
of
them
we
actually
found
a
bark
that
we've
then
also
fixed
in
the
rest
in
a
library.
That's
that
we
don't
model
full
rust.
There
are
still
a
couple
of
things
from
in
rust
that
we
that
we
didn't
handle.
One
of
them
is
trade
objects,
which
are
essentially
a
form
of
existential
types
and
rust.
A
We
don't
have
a
big
memory,
so
we
consider
things
to
be
sequentially
consistent,
but
we
do
have
a
notion
of
non-atomic
accesses
so
that
we
can
reason
about
data
races
and
we
don't
consider
drop,
which
is
kind
of
automatic
structure
and
they're,
actually
being
some
interesting
issues
there
as
well.
So
this
is
certainly
very
interesting
future
work
to
look
at
so
to
to
finish
up.
We
claim
that
logic.
A
A
A
E
So,
first
thanks
for
the
talk,
so
it's
kind
of
you
have
to
explain
that
if
you,
if
you
had
to
mutable
references
and
you
would
send
them
to
different
threads
and
both
resonate
them,
obviously
that
would
pose
a
problem,
and
that's
why
you
said
man
mutable
references
are
not
allowed
multiple
of
them.
So
now
the
question
is
from
from
my
experience
from
using
rust,
like
in
most
of
the
cases
of
course,
most
of
the
variables
and
data
structures
you
don't
send
to
others
writes
still.
E
You
cannot
use
multiple
mutable
references
and
now
the
question
that
that
I
kind
of
sometimes
head
is
is
this
restriction.
That
is,
that
has
some
kind
of
background,
so
that
would
would
something
break
down,
except
for
this
reading
part
if
you
were
to
use
multiple
mutable
refer
or
if
it
were
allowed
to
use
multiple,
multiple
mutable
references,
or
is
this
just
because
it's
considered
not
a
good
style
to
have
multiple
mutable
references.
A
Things
would
break
one
example
is
interpreting
validation
if
you
have,
if
you
have
a
mutable
reference
or
any
kind
of
reference
into
a
vector,
but
then
also
have
a
mutable
reference
to
the
vector
as
a
whole
like
empty
it.
Now,
you're
in
a
reference
is
broken,
so
so
this
completely
serves
iterator
imitation
a
static
way.
Another
example
is
Russa
has
some
types,
so
you
can
actually
change
the
type
of
memory
by
switching.
Sometimes
the
implement
is
unions,
overlapping
memory.
We
can
change
the
type
of
a
particular
location
in
memory
by
switching
to
a
different
variant.
A
D
Very
nice
look
I
had
couple
of
questions.
One
is
I
was
pretty
intrigued
by
your
lifetime
separation
concept
in
your
paper
and
in
mind
way
reminded
me
of
cryptographic,
storage
protocols
where
you
have
revocation
of
keys
owned
by
a
owner,
so
they
can
define
different
access
controls
for
different
points
in
time.
So
have
you
considered
kind
of
using
the
theory
developed
in
iris
to
kind
of
look
at
verification
of
those
stories?
Protocols.
A
D
But
that
seems
like
a
promise
interaction.
Your
second
question
was
kind
of
related
to
the
previous
question,
which
is
you
mentioned
that
lots
of
users
of
unsafe
in
rust,
and
some
of
them
are
for
optimization.
So
did
you
discover,
during
this
project
some
reasoning,
principles
that
you
can
translate
back
into
type
system
concepts
to
to
kind
of
enrich
the
type
system
to
not
have
to
use
so
know
is
to
kind
of
take
those
unsafe
uses
and
transformed
into
safe
uses.
A
So
we
can
type
check
more
programs
than
last
can
maybe
not
strictly
more,
because
you
don't
have
a
formal
version
of
what
the
compiler
concretely
does,
but
there's
certainly
programs.
We
can
type
check
after
manual
translation
to
our
core
calculus,
which
the
rest
compiler
doesn't
have
check.
That's
that
the
rest
compiler
is
currently
being
extended
with
a
new
lifetime
mechanism
or
lexical
lifetimes,
which
is
extremely
powerful
and
seems
to
in
some
places,
even
be
even
more
powerful
than
what
we
model.
A
F
A
Model
mutex
by
doing
a
spin
lock
by
by
doing
a
spin,
lock,
okay,
so
we've
not
focused
on
on
the
actual
C
implementation.
It
was
more
we,
it
was
code
of
this
behavior,
which,
after
doing
mutual
exclusion,
gives
you
a
rust
like
type
level
mutable
reference.
Is
that
actually
a
sane
and
safe
thing
to
do
in
rust
and
that
what
we
fool.
B
A
A
Certainly
they
made
this
choice
liberally
because
they
tried
to
find
a
way
to
have
ref,
counted,
pointers
and
still
guarantee
League
freedom
and
didn't
find
anything
that
was
sane
and
then
decided
that
we
not
they
don't
guarantee
that
so
the
the
core
us
without
any
unsafe
code
could
probably
you
could
probably
prove
a
theorem
like
that,
but
rust-eze
adduced
the
factor
with
the
style
library
does
not
guarantee
League
freedom
and
anyway,
I
was
not
currently
set
up
to
prove
League
freedom.
So
we
couldn't
prove
that
anyway,.