[Applause]
hey guys undercard one of my key lesson
I want to talk about the challenges that
we face from building a virtual machine
for watch hands we want to run smart
contracts a lot you know we want to have
a bunch of conference security tools
want to be able to audit them one who's
that champion all checking for
verification and testing and so on
usually these are the December tools and
we also want to have like consensus what
we're building what is the exact
behavior of this virtual machine someone
held like a trusted runtime when deaf
adults mutations or implementers know
what you're building you wanted to be
perfectly on a big ewis we just want to
make sure we can avoid a consensus
buttons and again these are all things
that people tend to work on separately
someone's writing the documentation
someone is formalizing maybe my elevator
as well so I want to pitch another
approach which is would be applied in
the cane framework which is this idea
that you can kill efforts with case
notes basically the idea is that you
specify your language once and you drive
the tools that might sound like magic
but it's only what you're doing with the
parser you're not saying that the write
a parser it seemed at the time you're
probably writing a grammar and the tool
is going to generate of horses we we
take that same approach with languages
to the next level where you specify your
language in a formal assume
mathematically we could think of it as
Matthew to get its programming and from
there we generate parses interpreters
program verifiers we're working on a
bunch of tools like knowledge areas it's
on but the idea is like you specify your
line is once and then you get a little
I'd argue that its ambitious let's
derive all the tools from one
specification but it's also realistic
right never education
this and we're doing for quite a few
years I'd say he's pretty successful
with this so it's not it's not paperwork
it's ambitious but it's realistic so one
example you might have heard of this KTM
it's a formal specification of the EBM
in the K framework it's one more like
the yellow paper it's not the exact same
for Melissa but still it's executable so
if you could actually execute the
elevator so you can run it as I know it
basically and it reads like code with a
lot of documentation because we've opted
for a literate programming style where
you have bunch of documentation and then
the floor was all nice tools we generate
through this this pituitary console
Firefly which is sort of a travel
education to build a lot a bunch of dev
tools quite a truffle we generate dog
that the jello paper is some argue of
easier formal specification to read than
the yellow paper we do verifications a
bunch of every smart contracts ever
build immortal self a fault line and I'm
working on K wasn't which is just a
formalization of pipe assembly in the
case remote right now it's most respect
of cura webassembly very similar to the
officials back which is nice because
they work Joe they chose the same
formalism as we've been using parallel
so it's a testament it's a new form of
civil as Kolbe writing rewriting logic
or rewriting this it's these tiny
betting's we have a prototype embedding
for you awesome even though
by the state with building prototypes
we're working with the polka dot and
substrate to wrap up our verification
abilities to do for more education on
web accessibility and because k so
awesome
most EDM tools KTM tools will come you
awesome tools okay some massaging but
the idea is like we're doing blossom now
and when you want some kicks in or
everything to go and if it doesn't kick
in where we just do any other - I mean
work and that's what we're doing some
sweet there's this photographic you want
token after
[Applause]