►
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
Okay,
recording
is
going,
I
sent
out
the
hackmd
url.
Hopefully
you
all
have
it.
I
want
to
say,
welcome
to
florian
and
sabri
and
any
other
non
typical
participants,
jack
greenbaum.
I
guess-
and
I
don't
know
florian
do
you
want
to
kick
off
with
a
little
like
introduction
to
your
thinking,
there's
also
the
document
that
you
sent
out,
which
I
think
some
people
have
read.
Hopefully
would
that
be
helpful?
Would
you
like
to
do
that?
B
C
There
we
go:
okay,
yeah,
I'm
senior
director
of
engineering
in
the
green
hills,
advanced
products,
team
and
in
in
our
team
we
work
with
a
lot
of
safety,
critical
customers
in
automotive,
other
areas
of
transportation,
security,
critical
folk
space,
flight
applications.
Even
so,
that's
the
industry
that
we
come
from.
C
C
Yeah
and
I
joined
in
2003.
right
so
so
yeah,
that's
that's
where
I'm
coming
from
we've
been
doing
some
work
with
florian
and
james
and
sabri,
looking
at
how
rust
might
fit
into
the
type
of
applications
that
our
customers
build.
Our
our
main
two
products
are
our
development
tools,
the
multi-ide
and
green
hills,
c
and
c,
plus,
plus
compiler,
and
then
our
runtime
software,
the
integrity,
real-time
operating
system,
which
is
safety,
certified
security,
certified
and,
in
fact,
has
achieved
the
highest
security
certification
of
any
commercial
rtos.
B
B
B
So
that
was
yeah.
That's
the
quick
summary
of
all
this.
I
did
sorry
for
that.
Tim
is
also
from
green
hills
and
the
one
of
the
brave
people
that
have
been
speaking
to
us
about
that
yeah.
So
we
found
out
that
most
of
the
analog
that
most
of
the
analysis
and
most
of
the
safety
critical,
tooling
that's
built
on
top
of
rust,
is
actually
built
on
top
of
mirror,
which
was
one
of
the
the
most
interesting
findings
that
we
had
there.
A
A
Please
again,
please
we're
just
getting
started.
We
were
talking
about
the
the
kind
of
overall
approach
and
the
idea
of
working
on
critical
safety,
safety,
critical
systems
and
so
forth,
but
I
think
I
don't
know
so
that's
we
haven't
done
a
lot
yet.
I
think
we
were
going
to
start
going
through
the
kind
of
some
of
the
principles
or
talk
about
what
we're
trying
to
do
right.
D
B
So
that
was
not
not
only
a
discussion
with
green
hills,
but
also,
for
example,
if
you
look
at
what
the
egh
rubric
is
doing,
that's
mostly
based
on
me
are
like
all
the
public
research
projects
are
actually
centering
around
mirror.
So
when
we're
talking
around
about
verification,
we
found
that
we're
mostly
talking
about
we're
verifying
a
trunk,
an
already
transform
brush
program
to
mirror
that
was
generally
what
we
found.
B
That
does
not
mean
that
no
one's
looking
at
the
language
or,
for
example,
language
evolution.
This
is
some
a
little
bit
further
down
in
the
in
the
document
that
I
wrote.
Some
more
structured
approach,
for
example,
on
the
trade
system
like
like
chalk,
is
currently
like,
that's
being
currently
currently
being
implemented
with
chalk
or,
for
example,
polonius
as
a
more
rules
based
a
lifetime,
checker
would
probably
help
at
specifying
them
for,
for
example,.
E
E
E
Not
necessarily
because
we
found
that
verification
the
contracts
you
make
for
verification
also
can
be
very
useful
for
runtime
checking
and
fuzzing.
So,
ideally,
in
fact
you
want
a
language
where
sort
of
you
have
different.
You
have
subsets
that
you
know
maybe
run
time,
checkable
and
subsets.
That
may
be
verifiable,
but
you
can
get
a
lot
of
the
benefit
for
sort
of
both
through
the
same
language.
E
G
Yeah,
I
think
the
the
the
large
sort
of
notion
here
is
that
mirror
semantics
are
just
far
simpler
than
rusts,
and
you
know,
and
so,
if
you're
looking
to
to
creating
this
sort
of
formal
semantics,
mirror
sort
of
makes
sense,
because
everything
reduces
the
mirror.
At
some
point,
and
so
that's
sort
of,
I
think
the
larger
thinking.
But
I
also
kind
of
wanted
to
to
go
back
to
daniel's
point,
which
is
the
contract.
G
Language
is
sort
of
in
scope
for
a
lot
of
around
some
of
the
things
that
we're
working
on,
but
is
it
sort
of
the
the
primary
goal
of
this
proposal,
which
is
specifically
around
mirror
and
sort
of
rust
itself
being
able
to
make
formal
verification
of
rust
programs?
More
ergonomic
is
definitely
in
scope
for
just
our
thinking
and
sort
of
the
initiative
that
we're
trying
to
launch
off
the
ground
but
again
sort
of
out
of
scope.
For
this.
F
F
Or
are
you
talking
about
trying
to
completely
prove
the
behavior
of
a
program
like
the
mirror,
precisely
matches
this
specification
and
does
absolutely
nothing
that
isn't
in
this
specification,
total
proof
or
very
narrow
property
proof
or
somewhere
in
between
that
that's
the
flavor?
I
was
looking
for
yeah.
G
E
Okay,
based
on
what
we've
done
sort
of
at
aws
with
c,
and
what
we're
currently
sort
of
looking
to
build
similar
capabilities
for
us,
there's
sort
of
both
directions
right.
So
there's
a
lot
of
work
where
you
want
to
say
like
does
this
program
have
undefined
behavior
right
so
unrest,
for
example,
a
program
that
has
some
unsafe
code?
E
Can
we
possibly
have
undefined
behavior
right,
and
so
you
want
to,
for
example,
take
the
exact
mirror
semantics
put
that
into
something
like
a
model
checker
and
then
have
a
model.
Checker
tell
you
whether
undefined
behavior
states
are
reachable
and
there's
the
other
extreme,
which
is
the
stuff
that
we've
done
with
like,
for
example,
some
of
our
crypto
code,
where
you
want
to
say
like
is
this
bit
for
bit
identical
to
the
specification
in
the.
G
E
Right,
and
so
they
are
you're
willing
to
invest
a
huge
amount
of
human
effort
to
prove
that
the
only
bits
that
can
be
emitted
from
this
exactly
match
what
you
have
in
some
formal
specification,
but
there's
a
lot
of
code.
That
sort
of
you
know
it
really
depends
on
the
business
case
for
the
code
right.
If
you
have
code
that
you
really
care
about
the
precision
like
crypto,
it's
worth
doing
that
if
you
have
code,
that's
like
you
know,
handling
some
lambda
functions
off
the
wire.
A
So
I
want
to
try
to
focus
the
I'm
looking
at
the
clock
and
thinking
about
our
time,
and
it
seems
like
this
is
good
background
and
we
should
keep
having
this
conversation.
But
I
want
to
talk
a
little
bit
about
like
how
I
understood
what
what
we're
trying
to
get
out
of
this
meeting
is.
Basically,
we
know
we're
not
going
to
solve
all
the
problems,
certainly
not
in
45
remaining
minutes.
But
what
we
can
do
is
talk
about
what
are
the
most
important
things
to
be
talking
about
over
the
next
period
of
time.
A
And
how
do
we
want
that
to
proceed
right?
And
I
agree
with
sabri
that
that
if
we
want
to
enable
these
use
cases,
kind
of
what
we
need
to
be
doing
is
coming
up
with
some
some
definition
that
we
can
work
from
of
like
what
a
rust
program
means
and
mirror
is
a
good
starting
point.
Sort
of
the
the
components
seem
to
be
mirror
traits
types
and
maybe
like
layout.
A
That's
my
that's
my
usual
list
layout,
meaning
like
given
a
type
where
does
it
appear
in
memory,
and
we
could
talk
about
like?
Is
that
the
right
set
and
then
what
would
it
look
like
to
specify
those
things
when
we
say
mirror?
Do
we
mean
like
mirror
from
the
compiler
or
mirror
from
or
some
abstract
notion
of
mirror?
I
think
the
latter.
I
don't
know
those
are
some
of
the
questions
I
think
might
be
good
to
focus
on.
B
That
does
precisely
this
kind
of
analysis
you
want
to
look
at,
so
that
was
an
interesting
part
that
a
lot
of
people
that
we
interviewed
was
that
we're
actually
not
into
well,
certainly
some
taking
the
speed
out
but
more
on
actually
actual
gathered
and
committed
knowledge,
rather
than
rather
than
strict
stability.
And
can
you.
B
Is
we
believe
it's
now
time
to
bring
these
concerns
into
the
language,
evolution
and
and
think
about
them
and
also
bring
the
hands
to
actually
do
that,
and
we
think
it
would
be
a
huge
boost
to
the
language
of
that
where
concern
that
was
handled
to
a
certain
extent
at
the
core
sure,
if
any
validation
approach,
if
every
validation
approach
needs
to
be
implemented
by
the
bus
project
but
saying
like
mirror,
is
the
basis
for
a
lot
of
the
verification.
For
that
reason,
there's
a
we
can.
B
C
From
our
view,
we've
been
looking
for
what
is
the
normative
definition
that
we
can
do.
Compiler
assurance
on
starting
from
the
rust
source
language
seems
much
more
complex
than
trying
to
assure
from
mary
on
down
and
trying
to
provide
assurance.
The
other
way
does
the
language
is
the
language
well-defined.
B
E
Okay,
I
would
agree
with
that
also
so
having
like
work
on
building.
Some
of
these
tools
mirrors
a
great
representation
to
go
from
sort
of
has
the
right
level
of
information,
but
it's
very
we're
very
worried
about
making
sure
that
we're
sound
and
that
we
stay
sound,
and
you
know
I'm
more
than
willing
to
invest
engineering
time
in
keeping
up
with
changes.
E
But
I
want
to
make
sure
I'm
actually
doing
that
right.
So
it
would
be
great
to
know
sort
of
like,
as
mir
evolves
to
know
that,
like
we
are
actually
keeping
up
with
the
semantics
and
we
don't
have
stuff
where
you
know
our
tool
still
works.
But
the
semantics
have
changed
subtly
and
we're
now
giving
some
unsigned
results.
F
F
Do
you
have,
or
are
you
driving
towards
any
interest
in
producing
mirror
and
expecting
it
to
be
consumed
by
the
rust
compiler
when
it
wasn't
produced
by
the
rest
compiler,
which
would
be
a
substantially
larger,
ask
and
more
complex
surface
area?
Or
are
you
just
looking
for
a
standard
that
allows
you
to
safely
and
versionedly
consume
it
in
order
to
do
analysis
and
similar.
F
H
In
the
research
that
we
had
I'll
jump
in,
I
I
because
we've
had
some
conversations
with
folks
about
this
I'd,
say:
they're,
two
separate
goals
and
I'd
say
consuming
the
the
serialized
output
is
probably
the
more
important
of
the
two
goals
of
being
able
to
say.
You
know
these
subset
of
compiler
versions
are
using
mirror
12
and
this
one's
using
mirror
13
and
that
way
any
tool
that's
consuming.
That
can
say.
H
So
there
could
be
a
desire
to
feed
the
rust
current
front
end
into
a
different
non-lvm
back
end
and
then
maybe
at
some
point
in
the
future,
having
a
different
rust
front
end
that
could
be
fed
into
a
compatible
rust
back
end
that
are
speaking
the
same
version
of
that.
But
I
would
say
the
initial
more
primary
pressing
goal
would
probably
be
having
a
versioned
serialized
output
version
of
mirror
not
even
necessarily
mirror
exactly,
but
a
serialized
mirror
format
that
has
a
version
number
associated
with
it.
H
F
F
So,
if
that
were
the
ask,
I
think
we'd
want
to
have
a
much
more
detailed
and
careful
specification
of
the
interface
for
the
purposes
of
what
works
and
does
not
work.
But
that's
not
an
issue
if
we're
primarily
talking
about
consuming
the
output
of
rusty.
So
that
was
all
I
was
trying
to
find
out
thanks.
E
We
start
we
want
to
start
with
this
right
there
so
two
points
what
actually
so
to
begin
with
we're,
mostly
interested
in
consuming
mirror
and
then
translating
it
into
the
input
for
the
kind
of
model.
Checking
that
we
do,
but
one
phase
of
that
is
that
we're
likely
to
want
to
do
some
mirror
to
mirror
transformations
right,
for
example,
to
add
ghost
state
to
allow
us
to
track
properties
that
we're
looking
for,
and
so
those
often
make
the
most
sense
as
many
mere
translations.
E
So
having
a
nice
way
to
do
that
kind
of
transformation
would
be
nice.
The
other
thing
which
I
just
want
to
push
on
the
stack
is
a
concern
that
I
have
is
about
the
fidelity
of
mir
to
the
original
rust
in
particular.
If
we're
looking
for
things
like
undefined
behavior,
it's
possible
that
there
may
be
uv
that
exists
in
the
original
rust,
but
where
the
compiler
gave
some
implementation
defined
semantics
to
it,
and
so,
if
there's
a
way
to
say
like
I
really
want
like
don't
try
to
do
that
at
all.
H
Real
quick,
I
also
want
to
echo
the
mirror
to
mirror
transforms
for
the
safety
critical
space
as
well,
because
things
like
verifiable
optimizations
and
things
like
that.
If
we
have
sort
of
a
language
spec
to
do
that,
optimizations
are
a
tricky
thing
in
a
lot
of
the
higher
safety
critical
areas
and
having
an
easier
way
to
do.
Optimizations
on
a
mirror
to
mirror
level
could
also
be
an
interesting
thing.
A
G
Yeah
to
something
that
it's
actually
sort
of
outlined
in
the
document
a
little
bit
sort
of
like
what,
if
you
were
to
define
formal
semantics
of
those
translations,
then
you'd
be
able
to
test
right
those
transformations
and
make
sure
that
they're
also
sound,
and
you
know
they're
total
and
there's
no.
So
there
is
some
benefit
of
that
specification,
but
I
think
we
specifically
point
out
that
lightweight
specification.
G
Whatever
lightweight
we
decide,
the
lightweight
means
would
still
be
helpful
so
that
people
have
some
understanding
of
what
they
can
expect
and
that
so
that
we
can,
we
can
do
some
some
lightweight
verification
of
those
things.
I
think
that's
again
sort
of
an
aspirational
effort.
But
if
you
look
at
projects
like
comcert,
which
you
know
try
to
be
the
you
know,
we're
going
to
specify
all
of
the
optimizations
there's
interest
there
for
sure.
A
Ultimately,
this
effort
is
going
to
be
bigger
than
it's
going
to
evolve,
involve
different
parts
of
the
rust
org
right
and
a
large
part
of
the
practicality
of
what
solving
the
practical
problems
of
working
with
mirror
is
probably
going
to
be
involving
the
compiler
team
and
involving
a
certain
amount
of
like.
Can
we
define
libraries?
A
My
hunch
is-
and
I
don't
want
to
go
too
far
down
that
road,
but
the
best
way
to
do
this
would
be
to
have
a
separate
crate
that
defines
like
portable
mirror
or
something,
and
the
compiler
has
its
own
copy
of
mirror
and
there's
a
translation
between
them.
And
you
know
that
that
translation
gets
maintained
by
people
as
things
change
and
like
the
group,
I
could
imagine
a
group
working
and
developing
that
just
because
we
want
to
have
an
interface,
we
want
to
be
able
to
know.
A
We
want
something
with
more
stability
and
where
we
have
like
semver
on
it
right
and
I'm
not
sure
that
I'm
not
sure
if
that
is
going
to
be
one
copy
or
not.
But
I
also
think
this.
This
team
isn't
the
one
to
make
that
decision,
and
so
I
think
we
should
like
segregate
out
some
of
that
and
talk
a
little
bit
more
about
what
would
a
spec
look
like,
and
one
of
the
questions
that
was
raised
here
is
or
what
my
biggest
concern
honestly
is.
A
How
do
we
keep
the
laying
team
abreast
of
what's
happening
without
requiring
us
to
attend
all
the
meetings
and
not
just
the
lying
team?
Really,
but
I
mean
like
the
rust
community,
the
set
of
people
in
the
community
who
want
to
follow
along
and
who
have
the
time-
and
you
know
knowledge
to
do
so-
maybe.
B
B
This
is
why
we
want
to
have
the
conversation
on
the
on
the
project
around
the
project
teams
to
make
sure
that
especially
also
the
different
perspectives
on
this,
like
there's
interest
in
verified
optimizations,
both
from
the
safety
critical,
but
also,
for
example,
from
the
mission
critical
perspective
of
of
amazon,
so
that
I
believe,
there's
a
there's,
a
there's,
a
design
space
there
where,
if
you
talk
to
multiple
groups,
this
just
becomes
better.
Also
in
from
the
engineering
perspective.
C
D
D
So
I
think,
we've
already
sort
of
outlined
in
previous,
like
parts
of
this
dialogue,
that
this
story
is
not
just
about
the
mirror
in
terms
of
like
defining
the
bodies
of
code
inside
of
rust
functions,
but
also,
I
think,
the
type
system
and
references
to
that,
and
so
I'm
I
wanted
to
try
to
in
an
effort
to
at
least
have
some
idea
of
the
scope
here
and
how
it
might
blow
up
or
how
we
can
keep
it
contained.
Are
there
any
other
static
analysis
results
that
you
expect
to
be
part
of
the
serialized
format.
D
You'll
need
access
to.
I
think
I'm
thinking
in
particular
of
the
borrow
checker
or
the
region
inference
I'm
that
may
or
may
not
be
part
of
the
type
system
that
we'll
need
to
define.
So
I
want
to
say
upfront
to
get
an
id
up
front
about
whether
that's
going
to
have
to
be
part
of
the
format.
That's
going
to
be
included
here
or,
if
you
don't
know
it
might
be
an
unknown
unknown.
That's
fine
too!
I
just
wanted
to
first
say
it
up
out
loud
yep.
I
have
a
little
bit.
G
Of
context
here-
and
it
depends
on
who
you
talk
to
and
what
their
needs
are,
some
folks
are
are
interested
in
a
mirror
that
is
to
be
borrowed,
checked
just
to
sort
of
describe
it
that
way.
But
then
there
are
some
folks
who
are
interested
in
mere
sort
of
post
bar
checking
posts
monomorphization
so
that
they
can
assume
they
can
consume
it
effectively.
After
rust,
guarantees
have
been
executed
and
there's
some
proof
erasure
in
in
a
way.
So
I
think
this.
D
There's
there's
a
point
between
the
two
that
I
want
to
make
sure
I
also
at
least
make
clear
here
when
you
say
the
the
mere
2b
borrow
check,
but
you
could
interpret
that
to
mean
you
know
we
wrote
our
own
borrow
checks,
someone
else.
A
third
party
wrote
their
own
bar
trigger
and
they're
gonna
apply
it
to
the
mirror.
That
is
different
from
like
having
a
a
serialized
proof
that
the
of
what
the
rust
compiler
itself
did
its
borrow,
checking
and
validating
that
right
and
that's
right.
G
This
is,
I
guess,
so
you
say,
consumption
right
so
consuming
meaning
this
is
output
from
the
rest,
compiler
that
we're
then
going
to
use
for
automated
reasoning
or
tools,
and
things
like
that.
Yes,
so
I
think
in
that
case,
yes,
it
would
be
sort
of,
after
after
bar
checking
after
an
expansion
and
transformation,
because
we
do
want
that
proof.
But
again,
I
think
you
will
hear
different
things
from
different
people
just
to
make.
A
A
E
That
can
be
very
because
one
of
the
things
that
really
absolutely
killed
the
performance
of
these
reasoning
tools
is
having
to
deal
with
memory
in
the
heat
and
aliasing,
so
anything
that
we
can
reuse
from
any
analysis.
That's
been
done
inside
the
compiler
about
aliasing
to
dramatically
improve
the
scalability
and
also
can
be
useful
for
correctness
right
if
we
know
that
the
borrow
checker
assumed
that
these
two
things
could
never
alienate,
and
then
we
can
find
a
path
where
they
did
now.
We've
shown
a
potential
bug,
so
both
directions
are
useful.
There.
D
Okay,
so
I
guess,
like
my
point,
is
that
then
it'd
be
good
to
at
least
have
some
bound
on
the
number
of
static
analyses
that
you'd
want
either
again
it
also
can
come
down
to
rk.
Are
you
expecting
just
a
statement
from
the
compiler
saying
I
borrow
checked
this
successfully
or
like
a
proof
that
could
be
validated
right
and
that's
those
are
different
or
just
the
static
analysis
results
without
a
so-called
proof
and
the
third
party
tool
would
if
it
needed
to
or
wanted
to,
could
attempt
to
reconstruct
those
results
or
validate
themselves.
D
But
the
point
right
there's
a
difference
there
between
just
taking
the
borrow
checkers
output
as
a
given
saying,
okay,
this
is
the
lifetimes.
You
figured
out,
I'm
not
going
to
worry
about
validating
them,
I'm
just
going
to
use
them
as
my
own
tools
routine,
which
is
a
totally
different
kind
of
problem
than
having
a
construct
then
making
the
compiler
construct
a
proof
that
would
have
to
be
validated.
A
What
what
the
like,
what
the
pristy
work
did
felix
is
it
took
the
output
and
used
it
to
generate
the
proofs,
as
I
firing,
if
I
recall
that
or
like
used
it
to
generate
some
of
the
things
that
are
then
fed
into
the
proof
checker
and
the
idea
was
it
also
along.
The
way
was
proving
that
the
bar
checker
was
sound,
because
if
the
proof
checker
failed
to
find
a
proof
like
those
things
ought
to
make
the
proof
succeed
in
short,
but
it's
not
that
it
trusted
the
broadcast
right.
A
B
The
question
is:
how
much
of
that
needs
to
be
specified
like?
Is
it
specified
as
a
minimal
guarantee?
A
borrow
checker
for
us
needs
to
do
at
least
this,
or
do
you
go
for
a
specification
that
nails
down
all
the
rules,
but
in
that
case
would
potentially
bar
future
research
that
might
make
the
boiler
checker
a
lot
more
convenient.
Someone
finds
a
yeah,
so
so
this
is
something
that
that
needs
to
be
taken
under
account.
A
I
think
the
other
thing
is
like
we're
kind
of
not
there
yet
in
some
sense,
I
think
if
you
take
stack
borrows
like
what
part
of
what
ralph
was
shooting
to
do
with,
that
was
to
define
a
kind
of
base
layer
of
undefined
behavior.
That
must
under
no
circumstances
happen
right
and
then
the
question
is
to
show
that
the
biochecker
guarantees
that
that
that
behavior
doesn't
happen,
but
there's
some
space.
It's
a
conservative
analysis.
G
Right
and
I
think
to
everyone's
point,
like
I
used
the
word
proof
in
a
in
a
maybe
less
than
rigorous
way
here
in
that
is,
if
people
understand
that
the
bar
checker
is
sound
because
we
have
evidence
either
through
you
know,
another
project
or
we've
actually
performed
the
verification
work.
Then
you
know
the
overall
sort
of
concept
here
is
improving
trust.
G
A
B
Go
the
goal
from
our
side
is
actually
to
continue
that
conversation
and
bring
it
somewhere
in
the
open
and
on
project
grounds,
also
for
multiple
reasons.
First
of
all,
we
did
a
lot
of
research
and
we
think
there's
a
it's
a
good
moment
to
start
that,
there's
a
limelight
on
rust,
there's
industry
interest.
I
think,
showing
that
there's
interest
from
rust
in
those
interests
is
also
good
and
starting
work
earlier
always
has
the
advantage
of
not
being
rushed.
A
I
think
yeah.
That
seems
like
a
good
thing
to
look
for,
and
I
guess
what
I
would
be
interested
in
from
my
perspective
is.
The
very
first
thing
would
be
kind
of
this
road
map
like
something
some
kind
of
document
that
sketches
in
more
detail.
What
what
are
the
things
to
be
produced
and
what
are
some
other
concerns
and
not
all
the
way
down
the
line.
Just
what
are
the
first
few
first
one
or
two
things
we
want
to
actually
do.
That
seems
sufficient.
A
Dive,
not
this
not
live,
but
to
talk
about
some
of
the
more
complex
topics
like
unsafe
code
and
rules
around
it
and
are
those
things
in
scope
or
out
of
scope
for
those
first
few
documents.
And
when
do
we
think
they'll
become
important,
because
I'm
trying
to
figure
out
how
to
like
how
this
interact,
for
example,
how
this
effort
interacts
with
unsafe
code
guidelines
in
my
head,
they're
very
close.
H
H
So
I
think
there
are
a
lot
of
things
that
would
make
sense
to
start
collecting
under
a
similar
umbrella.
Whether
this
is
increasing
trust
for
things
like
defining
unsafe
code
for
defining
certain
things
like
that
or
or
at
least
exploring
what
is
and
isn't
covered
and
better
kind
of
stating
the
guarantees
of
what
are
and
aren't
covered
and
and
where
those
fall
on
the
road
map,
so
that
people
who
are
maybe
interested
in
that
can
either
chime
in
and
and
help
prioritize
that
with
hands
or
or
funding.
H
Until
someone
brings
new
information,
I
think
definitely
makes
a
lot
of
sense
here,
because
I
think
there
are
parallel
efforts
of
folks
trying
to
either
improve
the
trustability
of
rust
or
working
on
certain
aspects
of
that,
and
some
of
those
are
disjointed
efforts
and
some
of
those
are
done
in
private
and
I
think,
having
sort
of
a
beacon
inside
of
the
project
is
going
to
be
helpful
in
that
regard.
For
my
position.
I
How
much
the
compiler
is
going
to
help
people
manually
verify
things?
There
are
different
markets
with
different
approaches
to
verification,
so
in
automotive,
for
instance,
there's
a
huge
body
of
code
and
manual
inspection
of
the
binary
output
isn't
practical.
So
you
see
in
standards
like
iso
26262,
where
you're
encouraged
to
trust
the
compiler
and
compiler
certifications
are
important
to
automate
that
process
in
other
standard
industries
like
aerospace,
d178,
certification
for
software
there's,
actually
a
substandard
do
330.
I
I
believe
it
is
that
makes
it
pretty
clear:
you're
not
really
allowed
to
trust
automated
tools,
and
what
you
want
from
your
automated
tools
is
enough.
Diagnostic
information
that
lets
you
show
manually
verify
that
the
tool
did
the
thing
you
think
it
was
going
to
do,
but
that
check
is
manual
so
in
india
178.
We
don't
actually
trust
our
compiler.
We
have
tools
in
our
compiler
that
lets
that
verification
process
be
done
manually
to
see
how
that
translation
from
source
to
binary
happens
and,
of
course,
any
point
where
the
compiler
introduced
is
non-syntactic
code.
B
I
think
there's
also
an
an
interesting
discussion
to
be
had
about
the
higher
you
go
on
these
kinds
of
trust
levels.
How
much
can
the
open
source
project
carry
and
how
much,
not
so,
just
to
be
clear
that
that
that
will
definitely
be
an
open
discussion
to
always
decide.
So
that's
why
we're
after
thinking
a
lot
about
it,
took
that
approach
of,
let's
think
of
what
we
can
provide
as
a
platform
for
this
efforts
that
also
maybe
to
cover
my
last
point
there.
B
We
can
maybe
also
reuse
to
make
development
of
of
rust
easier,
particularly,
I
was
thinking
about
when
we
think
about
chalk
as
a
formalization
of
our
of
our
type
system.
We
can
also
use
chalk
to
prototype
extensions
of
the
type
system
before
we
actually
build
it
into
the
compiler
full
if
you
got
that
factored
out.
So
we
do
not
only
need
to
think
about
this
as
a
additional
load,
but
maybe
a
different
design.
A
So
it
seems
like
the
next
step
is
to
create
the
charter,
for
like
a
project.
Group
right
is
that
that
would
be
destruct.
The
obvious
shape
for
my
view,
and
I
think
we'll
want
to
like
that
charter
will
inform
a
little
bit
who,
like
we
said
it's
cross-cutting
already,
who
else
we
loop
in
and
for
what
and
when
right.
A
A
A
I'm
just
wondering
a
little
bit.
My
other
rule
of
thumb
that
I've
been
using
lately
is
don't
make
a
group
until
the
group's
already
active
and
along
those
lines,
because
you,
you
know,
for
the
obvious
reason
that
sometimes
it
never
works
out.
I'm
wondering
what
can
we
do
like
to
some
extent.
That
charter
is
an
example
of
work
that
can
be
done
before
the
group
like
the
act
of
creating
it
is
sort
of
defining
the
group,
but
maybe
there
are
other
things
I
don't
know.
A
I
would
be
a
bit
wary
of
having
like
a
spec
for
mirror
that
lives
outside
the
rust
dirk.
I
don't
think
that's
a
great
universe
right,
but
on
the
other
hand,
I'm
not
like
there
could
be
worse
things
than
a
tightly
a
good
collaboration,
that's
not
official
until
it
gets
blessed
as
long
as
it's
really
good,
but.
G
G
You
know
into
a
group
where
we
can
figure
out
exactly
what
is
and
what
isn't
in
scope
and
and
then
figure
out
like
what
we
need
to
pull
in
and
who
we
need
to
pull
in
to
to
make
that
sort
of
initial
iteration
off
the
ground.
But
I
think
we
have
enough
information
to
get
that
ball
rolling
pretty
hard.
If
we
need
to,
we
should
probably
should
right,
because
I
think
there's
a
lot
of
industrial
and
entrance.
G
G
A
I
just
want
to
just
to
make
expectations
clear
like
to
the
extent
that
we're
we're
still
discussing
a
hypothetical
future
official
rest
endeavor
at
this
point.
It's
not
like
there's
no
decisions
being
made
right
now
or
anything
like
that.
I
feel
positive
about
it,
but
I
think
we,
the
act
of
creating
a
starter
and
figuring
out
who
we
need
to
talk
to,
and
so
on
seems
like
a
good
thing
to
just
clarify,
but.