►
From YouTube: a-mir-formality walkthrough (2022-07-06)
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
B
A
Now
not
only
sort
of
a
key
part
of
our
process
for
modeling
new
language
features,
but
also
for
like
sketching
the
implementation
structure,
because
a
lot
pretty
much
all
the
hard
problems
surface
at
this
level
as
well
right
the
easy,
the
easy
problem
so
to
speak.
Do
not
you
know
like
how
what
kind
of
pointer
do
we
use
and
what's
more
efficient
memory
layout
now
that
doesn't
show
up,
but
but
the
like
hard
problems
where
you
get
stuck.
B
A
B
A
D
C
A
A
I
don't
know
if
if
I
know,
Dominic
saw
it
I,
don't
know
Santiago
if
you
did
but
I
over
the
weekend,
I
implemented
a
new,
a
new
layer
so
used
to
be.
We
had
the
logic
layer,
I
realized,
I
should
name
these
with
numbers
or
something
because
right
now,
they're
in
like
a
random
order.
But
anyway
we
had
the
logic
layer
which
had
the
type
layer
on
top
that
defines
how
types
work,
the
Declaration
layer,
which
sort
of
doesn't
consider
function,
bodies
but
kind
of
has
stuff
at
the
function.
A
Everything
else
layer
and
defines
how
you
lower
those
into
logic,
the
mirror
layer
that
defines
mirror
type
check
and
and
other
stuff
and
also
I.
Guess,
interestingly,
I,
don't
know,
there's
sort
of
two
things:
I
realize
now
as
I'm
talking
squashed
into
the
mirror
layer
right,
there's
like
the
mirror
type
check,
but
also
the
kind
of
top
level
checking
the
main
check
function,
which
maybe
should
be
separated
itself
out,
because
that
includes
stuff,
like
coherence
and
so
on.
That
just
doesn't
really
feel
like
part
of
type
check.
A
But
anyway,
there's
those
things
and
then
I
added
this
extra
layer
called
rust
I
will
totally
relevant
to
you
as
well
and
the
main
dip.
The
main
thing
about
the
rust
layer
is
it's
supposed
to
be
the
topmost
layer
and
the
syntax,
and
everything
else
is
completely
separated
and
corresponds,
as
close
as
I
could
make
it
to
actual
rust
syntax.
So,
like
as
an
example,
here's
the
coherence
check.
A
A
A
So,
let's
see
where's
an
example,
I
would
say
this
corresponds
to
in
the
compiler
kind
of
AST
or
something
trying
to
find
an
example.
I
guess
this
one
will
do
you
know
this
is
a
function
Foo
with
a
lifetime
parameter
and
a
type
parameter
and
here's
the
input
argument
is
Ampersand
to
KT
Returns
the
ampersantic
at
aware
clauses
anyway.
A
The
rust
layer
has
its
own
concept
of
where
classes,
which
is
even
closer
to
user
syntax.
So
I
was
trying
to
get
rid
of
this
one
and
just
have
kind
of
chalk-like
syntax
and
then
user
syntax
that
gets
lowered
away
and
so
far
I'm
having
some
problems
doing
that,
because
some
tests
don't
pass
I,
don't
know
why
so
one
thing
we
could
do
is
sort
of
debug
why
these
tests
don't
pass,
but
that
might
be
kind
of
not
that
informative.
A
A
C
D
A
A
D
C
A
I
think
you're
at
the
right
spot.
I
think
we
do
want
to
eventually
align
Rusty
like
get
the
two
more
in
alignment,
so
that
there's
less
like
each
one
of
those
conversion
points
is
a
potentially
something
we
should
try
to
fix,
but
to
really
bring
the
two
into
alignment.
We
probably
have
to
actually
model.
A
You
know
take
as
input
the
here
and
model
mirrored
Construction
right.
That
would
which
I
think
we
should
eventually
do,
but
I
I
definitely
don't
want
to
bring
it
in
scope
right
now.
I'm
thinking
that
exact
example
is
an
interesting
one.
Just
yeah.
We
add
that
as
a
sort
of
synthetic
where
Clause
right
and.
D
A
Probably
not
harmful
anyway.
Okay,
that's
interesting,
because
yeah,
it's
interesting
that
we
don't
have
it
I,
know,
I
think
the
reason
we
have
it
is
because
it's
almost
a
convenience
thing
like
I
think
we
need
it,
because,
when
you're
type
checking
a
defaulted
function
body
you
get
to
assume
that
self
implements
the
trait.
A
Yeah,
we
don't
have
defaults
and
we
haven't
hit
that
stuff
yet,
but
so
that's
a
good
example
of
like
I
think
skipping.
It
is
fine
for
now
I
think.
Eventually
it
shouldn't
be
there.
There
should
be
a
like.
That's
actually
a
bug
that
we
should
fix.
I,
don't
know
which
way
we
should
fix
it,
but
they
should
be
the
same.
The
set
of
predicates
you
get
in
Rusty
and
the
set
of
where
Clauses
we
okay,
I'm,
not
sure.
C
A
I
see
your
point
we're
actually
because,
if
you
think
of
the
rust
layer
as
being
the
AST,
which
is
what
I
said-
and
this
is
sort
of
AST
to
here-
lowering
in
some
sense
this
lower
to
decal
function,
then
you're
generating
from
the
here
the
AST
and
that's
the
fundamental
problem.
You're
Reckoning,
with
more
or
less
the
mapping
isn't
perfect.
But.
A
Yeah
I
think
it's
something
to
keep
an
eye
on
I,
don't
know
what
I
think
the
right
answer
is
yet,
but
I
do
want.
I
do
feel
like
we
should
eventually
align
these
up
and
be
able
to
generate
from
like
one
spot
in
Rusty,
which
probably
means
more
like
the
ASD
level,
the
input
that
formality
expects
and
like
in
the
limit,
it
would
be
kind
of
cool
if
you
could
generate
it.
You
know
at
different
levels
like
we
could
generate
the
rust
level
or
the
decal
level
so
that
we
could
compare.
A
D
D
A
E
C
A
C
D
Like
the
lowering
of
the
bounce
clauses-
yes,
where
we
have
the
projections,
do
you
think
it
would
make
sense
to
also
lower
that
to
a
like
implements
per
clause
because,
like
that
is
what
happens
in
Rust
right?
If
we
have
the
or
if
we
say
that
I
usually
specify
both
like
the
yeah
and
the
projection.
C
D
A
Like
that
yeah
now
we
know
it
implements
the
trait,
and
when
projected
we
get
this
okay,
let's
see
what
happens
should
work,
although
I
noticed
there's
a
bug
yeah.
This
is
that
same
bug.
I've
hit
this
before
I
think
this
is
a
bug
in
in
Red
X.
You
see
how
it's
giving
me
this
error
too
few
ellipses
for
pattern.
Variable.
C
A
A
I
think
the
right
place
is
is
maybe
more
here
where
we
lower
the,
where
clause
so
that
it
would
generate
like
because
if
we
do
it
in
the
bounds
place,
that
means,
if
you
have
something
like
typhoon.
Iterator
item
equals
year.
32
we're
going
to
get
it
we're
going
to
expand
this
to
be
like
f
iterator,
where
f
is
the
type
Foo
and
also
f,
as
iterator
item
equals
u32.
A
Some
piece
of
code
like
function,
Foo,
f
era
that
doesn't
this
is
that
doesn't
apply
because
the
bounds
right
now
are
only
for
like
Associated
types,
basically
see
what
I'm
saying
so,
rather
here
where
we
convert
from
the
rust,
where
Clauses
into
the
internal
form.
Here
we
could
do
it
and
it
would
get
both,
but
we'd
have
to
modify
this
instead
of
taking
one
and
returning
one.
It
has
to
return
a
list
which
seems
okay,.
D
A
Right,
although
we've
talked
about
adding
it,
but
I
kind
of
let's
hold
off
I
think
it
might
make
sense-
and
this
is
probably
where
I
would
do
it.
But
what
I
the
other
way
to
go
about.
It
is
to
say,
foreign,
if
you
know
that
this
is
true
that
that,
like
if
we
know
that
we
can
normalize
this
Associated
type
to
this
user
type,
make
it
like
an
implied
bound
that
we
also
know
that
the
trade
is
implemented
which
is
kind
of
how
I
expect
it
to
be.
C
D
A
A
C
A
A
A
Yeah,
okay,
so
this
helper
function
tie
proof
scheme
says
this
is
really
for
for
writing
tests.
But
it's
a
good
idea.
It
says,
given
some
environment
and
some
variables
that
we
bring
into
scope
and
a
set
of
where
Clauses
that
we
can
assume
to
be
true.
We
try
to
prove
this
goal
and
we
get
back
a
set
of
schemes
which
are
basically
the
solutions
and
additional
constraints
and
things
that
apply
so
like
to
jump
back.
A
Something
like
there
exists
would
be
where
wreck
of
a
and
took
b
equals
to
k
or
something
I,
don't
think
it
I,
don't
know
whether
we
would
generate
the
equal
sign,
but
that's
the
idea.
So
you
get
the
main
goal
along
with
some
variables
that
you
can
instantiate
and
then
constraints
that
when
they're
solved
make
the
whole
thing
true
and
you
actually
get
more
than
one
potentially
because
we
don't
deal
with
ambiguity
very
well
in
this
code,
but
I'm
going
to
ignore
that
for
now.
A
A
A
C
A
A
A
A
A
A
A
True,
that's
okay,
because
it's
actually
the
right
thing
to
say
if
any
one
of
them
suffices
now
what's
missing
like
we
can
actually
just
stop
here
for
a
second,
we
should
probably
be
able
to
make
some
tests
because
what's
missing
now,
is
that
we're
supposed
to
then
take
the
like?
This
is
going
to
yield
a
whole
bunch
of
we're.
Gonna
have
a
whole
bunch
of
inference
variables
for
all
the
lifetimes
and
some
relations
between
them.
A
What
outlives,
what
and
so
forth
and
the
borrow
Checker-
would
come
in
now
and
say:
okay,
if
I'm
mutating,
especially
if
it's
Polonia
style,
if
I'm
mutating
a
a
variable
and
there's
some
live
starting
at
that
point
where
the
mutation
occurs.
There's
some
live
reference
which
may
have
borrowed
from
that
variable.
Then
that's
an
error
right,
but
I'm
just
going
to
skip
that
part
of
the
check,
so
not
really
doing
the
borrow
check
yet,
but
already
this
should
do
something
like
because
what
we
did
now
was
we
type
checked.
A
C
A
Yeah,
so
the
highest
level
view
is:
this
is
the
definition
of
or
this
Endeavors
to
be
hopes
to
become
kind
of
the
definition
of
rust,
in
some
sense,
a
formal
model
for
us
that's
accepted
and
that
it
does
not
currently
include
a
bunch
of
things.
It's
kind
of
got
most
of
the
trait
of
a
good
version
of
the
trade
Checker
better
than
rusts,
maybe
but
doesn't
have
a
borrow
Checker
yet
or
some
other
parts,
so
we're
poking
at
that
trying
to
fill
in
fill
in
the
bar
trigger
but
yeah,
as
you
can
see.
A
A
The
other
part
of
this
that
may
or
may
not
be
obvious,
is
this
is
being
implemented
in
Red
X,
which
is
oh
yeah.
There
we
go,
which
is
a
kind
of
dialect
of
Racket,
which
is
a
dialect
of
scheme.
So
this
weird
syntax
is
all
like
lisp,
syntax,
essentially,
but
anyway,
I
don't
know
it's
hard,
you'll
pick
it
up
for
you
hopefully,
but
any
case.
This
is
our
sample
input
function
that
takes
an
i32
and
returns
a
u32,
and
this
is
the
mirror
that
we're
type
checking.
A
These
are
the
local
variables
in
the
mirror.
Underscore
zero
has
Type
i32,
that's
the
return
variable
slot
underscore
one
has
Type
u32.
That's
the
argument.
The
first
argument
slot-
and
we
are
our
one
mirror
statement-
is
to
copy
one
into
zero
and
that
should
generate
an
error
because
i32
and
u32
are
not
compatible,
but
it
doesn't
because
we're.
Oh,
this
actual
unexpected
is
backwards
by
the
way.
That's
because
I'm
supposed
to
be
putting
it
like
in
the
other
order,
but
I
don't
because
I
like
it
better
this
way
anyway.
A
A
Okay,
so
indeed
we
now
get
the
test
is
passing
and
you
can
see
what
happened
right.
The
borrow
check
judgment
was
invoked.
This
is
the
program
definition
itself,
not
very
exciting,
or
not
very
easy
to
read,
but
this
final
bit
here
this
is
the
set
of
goals.
We
had
to
prove
that's
kind
of
interesting.
So
at
the
first
statement
within
basic
block
zero,
we
had
to
prove
that
u32
was
a
subtype
of
I-32.