►
Description
The recent surge of interest in secure memory management has sparked a renaissance of type safe systems programming languages. ATS is a statically typed ML that compiles to C and offers what almost no other modern systems language including Rust has: type safe pointer arithmetic. It is unabashedly large and complex featuring a dazzling array of verification tools from advanced type system mechanisms like refinement types right up a full proof language. This talk will use these features to show off the language's incredible power and control with non-trivial examples C interop, concurrency, and GC free low latency servers. No ATS experience is expected but the talk will move fast. Basic experience with C and a type system like Haskell's will be helpful.
Aditya Siram
COMCAST
I work as a Scala developer by day, but write Haskell, Shen, C, Rust and ATS by candlelight. My latest passion is languages like Rust and ATS that use sophisticated type systems that allow safe memory access and high level abstractions over unboxed data structures.
A
So
welcome
to
my
talk
on
systems
programming
in
80s,
so
before
I
start
with,
like
ATS
syntax
or
how
things
work
anything
like
that.
Here's
the
elevator
pitch
for
ATS,
it's
an
ml,
but
it's
not
a
standard
ml,
but
it's
got
algebraic
data
types
and
pattern
matching
and
all
that
good
stuff.
Functional
programming
is
fully
supported
because
tail
calls
are
actually
optimized
in
ATS
and
it
actually
also
supports
mutual
recursion.
A
But
the
thing
that
I
think
that
ATS
really
brings
to
the
table
that
sets
it
apart
from
all
the
other
languages,
is
exactly
the
same
performance
and
memory.
Predictability
of
C
notice,
I
didn't
say
that
it
runs
as
fast
as
C
or
uses
as
little
memory
of
C
I'm,
making
a
stronger
statement
than
that
I'm
saying
you
have
the
exact
same
control
as
C
all
that
stuff
that
you
do
in
C,
pointer,
arithmetic,
allocating
D,
allocating
freeing
stack
allocation.
A
All
of
that
stuff
that
comes
back,
but
there's
this
whiz-bang
type
system
that
makes
all
that
safe.
So
if
you
use
the
type
system
right,
you'll,
never
walk
off
the
end
of
an
array,
you
will
never
double
free
something.
You
will
never
have
dangling
stack
pointers
and
you
will
always
free
all
your
resources
and
I.
Think
that's
a
really
powerful
thing
to
have
it.
A
Just
D
compiles
to
C
and
except
for
tail,
calls
there's
no
real,
optimization
and
GCC,
or
your
favorite
C
compiler
does
the
rest,
which
is
why,
for
the
longest
time,
it
was
always
on
top
of
the
language
benchmarks.
It
wasn't
always
in
the
top
four,
if
I
was
always
like
C
C++,
ADA,
80s,
Fortran
and
now
rust
right,
but
for
some
reason
it
was
taken
down
in
2015
and
kind
of
pisses
me
off.
A
I've
know
what
actually
I
now
know
why
I
was
taken
down,
because
somebody,
the
audience
just
told
me
but
I,
didn't
know
why,
until
just
now,
but
a
couple
of
big
things
that
like
ATS
brings
to
the
table
are
like
linear
logic
to
manage
resources.
So
what
is
linear
logic?
So
if
you
create
a
resource,
you
allocate
memory,
you
open
a
file,
handle
you
open,
a
database
handle
that's
a
resource.
So
when
you
create
that
at
the
type
level
you
get,
this
thing
called
a
proof
object.
A
proof.
A
There's
this
pipe
and
to
the
left
of
this
pipe
is
this
thing
called
awesome
proof.
Awesome
proof
only
exists
at
the
type
level.
So
when
I'm
trying
to
read
from
that
file,
I
have
to
pass
that
awesome
proof
back
into
the
read
file
so
that
the
type
system
knows
that
the
file
descriptor
is
still
open
and
when
I
close
the
file
I
pass.
This
proof
in
that
proof
gets
consumed
and
is
no
longer
available
anywhere.
A
So
that
means
that,
even
though
file
descriptor
may
be
in
scope,
if
that
proof
has
been
consumed,
there's
no
way
for
another
function,
to
read
off
of
a
bad
file
handle
or
a
bad
memory
address,
or
anything
like
that.
An
80s
really
doubles
down
on
this
for
memory.
So
there's
like
specialized
syntax
that
says:
there's
a
pointer
at
this
address
of
this
size
of
this
type
that
may
or
may
not
be
initialized.
That's
like
five
characters,
or
something
like
that.
So
and
this
is
how
type
check
pointers
matech
works
in
80s.
A
This
is
how
you
can
never
read
off
the
end
of
an
array,
because
you
don't
have
a
proof
for
it.
The
other
big
thing
that
ATS
brings
to
the
table
is
this
idea
of
refinement
types.
So
refinement
types
are
a
way
of
constraining
a
large
type.
So
here's
this
function
foo
it
takes
an
int,
it
does
a
huge
type.
A
It
can
go
anywhere
from
0
to
like,
whatever
the
max
value
of
enters
on
your
system,
so
want
to
constrain
that
sometimes
so
you
modify
that
with
this
short,
it's
called
a
sort
in
80s
such
that
sort
as
an
INT,
where
n
is
greater
than
zero
and
n
is
less
than
10.
So
what
this
means
is
that
you
can
never
call
foo
with
an
integer,
that's
not
between
zero
and
ten.
The
type
checker
makes
you
do
that.
A
A
By
definition,
it's
funded
in
part
by
the
NSF
there's
one
P
I
in
Boston
University
like
doing
99%
of
the
commits
right.
So
when
you
put
all
these
things
together,
the
first
thing
that
goes
out
the
window
is
programmer
organ
onyx
all
right.
So
80s
is
a
tough
language
to
work.
It's
really
hard,
there's
no
easy
story.
There's
no
new
comer
onboarding
right!
A
A
So
the
easiest
way
to
get
started
with
80s
is
I.
Think
with
the
sea
Interop.
So
here's
a
generic
swap
function
and
see
that
swaps
to
avoid
pointers.
Yes,
I
realized
sending
size
T
as
an
argument
as
bad.
Don't
ask
me
on
that
one,
because
the
point
is
that
all
I
have
to
do
to
include
that
into
an
80s
file
is
stick
it
inside
of
these
percentage,
curly
delimiters
and
basically,
when
the
C
code
generator
gets
to
that
point.
It
just
takes
whatever's
inside
of
those
delimiters
and
jams
it
into
the
output
file
right
there.
A
It's
exhibits
exactly
that
simple
all
right
and
here's
a
foreign
function
call
to
that
swap
function.
It
takes
two
pointers
and
a
size
T,
and
the
thing
to
notice
here
is
that
all
of
this
all
of
the
base
types
in
80s
are
exactly
the
same
as
C
pointers
are
pointers,
size,
teaser,
size,
T's
incidence,
Long's
are
lungs.
There
is
no
marshalling
and
unmarshal
overhead,
we're
also
going
to
need
malloc
and
that's
a
size
T
that
returns
a
pointer
right,
but-
and
here
we
run
it.
A
Okay,
so
I'm
allocating
a
couple
of
chunks
of
memory
and
I'm
swapping
it
cool
here,
I'm
allocating
an
integer,
all
good
lovely
here,
I'm
allocating
a
double
that's,
not
good,
and
here
I'm
calling
swap
and
telling
it
that
both
things
are
double.
That's
super
not
good
and
I'm,
not
even
cleaning
up
right.
A
Okay,
so
80s
can
totally
mimic
see
bugs
and
all
you
can
port
your
Z
code
to
the
highest
fidelity
to
80s
by
just
you
can
port
it
line
by
line.
If
you
want
to
the
type
system
goes
to
11.
It
goes
all
the
way
down
to
C.
Okay.
So
this
the
upside
is.
This
facilitates
gradual
migration.
In
a
way,
that's
actually
I
think
easier
to
do
than
something
like
trust.
You
know
you
can
port
the
entire
Linux
kernel
over
to
ETS
if
you
wanted
to,
but
we
can
do
better
than
that.
A
A
It's
like
okay,
you
have
to
tell
me
whether
it's
a
size,
something
or
you
don't
know
what
the
size
is
and
that's
the
key
word
for
I
have
no
clue
what
the
size
of
that
thing
is
because
the
generic
argument,
okay,
so
I'm,
passing
in
an
address
where
the
address
has
to
be
greater
than
no
another
address
where
the
address
has
to
be
greater
than
now
and
now
the
actual
arguments
right,
I
have
an
eye
which
is
a
pointer
to
a
non-null
address.
I
have
a
J
which
is
a
pointer
to
a
non-null
address.
A
I
have
the
S,
which
is
a
size
argument
that
takes
this
type
size
of
underscore
t
that
is
parameterised
on
the
tee
at
ype
type
that
I
just
passed
in
in
order
to
be
type
safe
about
what
kinds
of
types
of
engineering.
So
I
can't
just
like
pass
in
five
as
a
size
argument
to
like
the
swap
function.
That's
and
then
we
see
that
familiar
pipe
again.
So
remember
in
the
example
where
I
was
reading
from
a
file,
descriptor
I
was
using
that
pipe
2d
structure
approve.
A
So
when
open,
when
open
file
returned
a
file
descriptor,
it
also
returned
a
proof.
I
can
also
use
the
similar
syntax
to
pass
improves.
So
here's
special
syntax
that
says
that
there's
something
of
type
a
at
address,
l1
I'm
passing
in
that
proof
and
something
of
type
a
at
address,
l2
also
passing.
In
that
proof
the
return
type
is
void,
but
it
also
returns
two
proofs
that
there's
an
a
of
l1
and
an
a
at
l2.
Why
does
it
do
that?
A
Because
ATS
by
default
will
consume
proofs
if,
unless
you
tell
it
not
to
those
proofs
are
gone
and
not
available
for
use
anymore?
So
if
you
actually
want
to
use
those
briefs,
you
have
to
return
them
by
the
way.
There's
a
special
there's
special
syntax
for
everything.
But
there's
like
special
syntax,
we're
saying:
don't
touch
these
proofs.
They're!
Fine,
don't
worry
about
it,
but
to
be
explicit,
that's
how
our
ups
works.
A
So
here's
malloc
make
ourselves
some
space
pass
in
that
one
size
type
parameter
past
net
size
argument
which
is
parameterised
on
size
of
a
on
size
of
t
and
pass
back
a
pointer
to
some
location
L
such
that
there
is
something
of
type
a
at
L
that
is
possibly
uninitialized.
That's
what
that
question
mark
means,
or
it
gets
better
and
an
address,
that's
greater
than
null
okay
cool.
A
So
now
we
have
our
main
function:
we're
allocating
an
integer
we're
getting
it
we're
getting
back
a
pointer
to
that
integer
I
and
a
proof
that
I
exists,
allocating
an
integer
getting
a
pointer
to
that
and
a
proof
that
that
exists.
That's
J
and
now
I
want
to
set
that
pointer
to
something
I
want
to
set
I'd
1,
so
I
said
I
don't
want,
but
I
also
have
to
pass
in
a
proof
that
I
exist.
It
consumes
that
proof.
A
A
Oh,
that
should
be
PF,
j,
1,
sorry,
typo
and
hands
back
a
it's.
What
it's
a
void
function
it
hands
back
a
proof
of
p,
fi,
2
and
PF
j
2
right,
because
we
need
those
to
free
the
resources
here.
I'm,
freeing
I
passing
in
that
proof
of
p,
fi,
2
and
3
and
J
passing
in
that
proof
of
p
FJ
2.
If
I
didn't
have
those
freeze.
A
That
would
be
a
type
error,
because
any
unconsumed
proof
left
lying
around
after
the
program
is
complete
is
a
type
error,
because,
according
to
ATS,
that's
a
leaking
resource
of
some
sort
somewhere.
You
have
to
clean
up
all
your
proofs,
like
you
have
to
clean
your
blank,
because
there's
starving
type
systems
that
don't
have
proofs
or
something
so
the
same
thing.
I,
don't
free
that
I
get
I,
get
a
type
error,
I
pass
in
something
size
of
something
other
than
it.
I
get
a
type
error:
I!
Don't
pointers
that
I
get
a
type
error.
A
A
Your
type
system
is:
please
test
your
code,
cuz,
there's
something
that
it
doesn't
see,
but
here's
the
original
code,
here's
all
the
code,
it's
dedicated
just
to
proof,
threading
right
and
there's
some
hash
blur
in
the
bag
going
type
level,
state,
monad
or
whatever
you
know,
but
nts's
like
lol.
How
about
implicit,
proofs
and
syntactic
sugar,
because
that
solves
everything?
So
here's
an
idiomatic
swap
in
80s
that
bank
p1
syntax
means
there's
a
pointer
called
p1.
A
Bang
means
dereference
this,
but
first
look
around
and
scope
for
a
proof
that
might
work
and
use
it,
which
is
absolutely
no
bug
vectors
here
whatsoever.
But
but
the
story
is
that,
like
implicit,
some
syntactic
sugar
solve
all
UX
problems.
So
remember
that
if
you're
designing
a
if
you're
designing
a
language.
A
Let's
take
a
huge
step
back
at
this
point.
Anybody
here
overwhelmed,
because
that
was
a
crap
ton
of
syntax
right,
brief,
there's
more,
but
it's
coming
and
I
haven't
even
shown
you
the
type
errors.
Yet
what
and
I'm
not
going
to
because
they
look
like
those
like
like
taunting
code
messages
that
serial-killer
send
the
cops.
That's
it's
it's
rough,
but
at
the
same
time,
I
still
like
think
that
you
should
look
at
ATS
not
for
hey,
adopt
us
now,
but
this
idea
of
passing
proofs
around
is
so
powerful.
A
I
think
I
think
it's
the
future
of
systems.
Programming
like
rust,
has
this
idea
of
linear
logic
right,
but
all
of
the
linear
logic
stuff.
The
cool
stuff,
is
back
behind
sort
of
the
lifetime
analysis
mechanism
and
sort
of
the
borrowed,
checker
and
stuff
like
that.
I
want
first-class
access
to
those
proofs.
A
Okay,
like
I
said:
ATS
has
first-class
support
for
recursion
and
in
fact
it
encourages
recursion,
unlike
other
systems,
programming
languages,
so
other
systems,
foreign
languages
don't
like
recursion
because
it
stops
over
the
C
stack.
This
is
also
true.
Ats
encourages
it
because
it
allows
the
type
checker
to
prove
things
by
induction.
So
here's
a
factorial
function
in
ATS,
there's
a
lot
of
group
there.
So
let's
look
at
the
essential
complexity
here,
there's
a
top-level
function:
factorial
there's
an
inner
function
loop.
You
kick
off
loop
with
1.0
and
I
and
as
you've,
all
probably
surmised.
A
A
We
propagate
that
constraint
to
the
inner
loop
and
the
inner
loop
takes
up
an
accumulator
which
is
a
double
and
an
I
which
is
an
int
parameter,
that
constraints
saying
it
has
to
be
greater
than
equal
to
1,
and
this
funny-looking
thing,
hello,
more
syntax
called
to
a
termination
metric,
a
termination
metric.
The
thing
inside
that
angle
bracket
is
a
number
or
an
arithmetic
expression
that
you
have
to
show
the
type
checker
is
strictly
decreasing
on
every
recursive
call.
A
A
Don't
worry
about
why
it's
case
we'll
get
to
that
in
a
second
or
maybe
we
want
I,
don't
know
if
it's
one
just
hand
back
the
accumulator,
if
it's
not
one,
when
it's
greater
than
one
make,
the
recursive
call
multiply
the
accumulator
by
I
and
decrement
I.
The
most
interesting
thing
about
this
example
is
not
that
it
works
is
what
happens
if
you
leave
stuff
out
if
I
leave
out
that
one
I
is
greater
than
one.
A
That's
a
type
error,
because
it's
going
to
say
you
have
this
constraint,
saying
that
I
has
to
always
be
greater
than
or
equal
to
one
more.
Interestingly,
if
I
do
anything
other
than
I
minus
one.
If
I
do
I,
if
I
do
I
minus
three,
the
solver
is
smart
enough
to
say
that
you
might
skip
right
past.
One
and
I
can
never
ever
show
that
this
is
going
to
be
greater
than
or
equal
to
one.
A
Okay.
So
the
next
big
thing
is
view
types
so
view
types.
Are
this
thing
that
connects
linear
resources
to
algebraic
data
types?
Remember
told
you,
80s
was
an
m/l,
so
we
want
to
be
able
to
use
all
of
this
like
functional
programming,
abstraction
goodness
to
control
these
linear
resources.
And
that's
what
view
types
do
for
us
so
to
see
what
a
view
type
is
here's
the
problem.
This
is
the
swap.
This
is
a
swap
definition
that
we
saw
earlier
taking
away
some
of
the
duplication,
here's
what
we
have.
We
have
a
type
of
unknown
size.
A
We
have
an
address
greater
than
null.
We
have
a
pointer
to
that
address
and
some
proof
that
there's
something
of
type
a
at
that
address.
This
comes
up
a
lot
right.
I'll
pointer
to
something
that
you
want
to
know
is
not
null
that
has
something
inside
of
it
right.
If
we're
gonna
work
with
ATS
at
a
higher
level,
we
need
to
somehow
package
all
these
things
up
and
the
way
to
do
that
is
with
this
thing
called
a
short
def
and
a
V
type.
Def
I
didn't
name
these
things.
A
So
a
sort
def
basically
takes
that
constraint
and
gives
it
a
name
I'm,
calling
it
age
in
fact,
I'm
not
calling
it
a
GZ.
It's
called
a
GZ
because
that
stands
for
address
greater
than
zero,
okay
and
a
view,
type
definition
that
takes
that
proof
and
that
pointer
and
packages,
those
up
together
with
a
constraint
on
it
that
the
address
can't
be
no,
and
we
call
that
safe,
pointer
and
parameterize
that
with
something
okay.
A
A
A
So
here
is
the
the
at
the
algebraic
data
type
of
a
list
of
view
types,
a
list
of
linear
resources,
cleaning
some
of
this
stuff
up.
This
should
look
relatively
familiar
so
instead
of
data
type,
I
have
data
view
type,
but
I
still
have
two
constructors
there,
a
no
constructor
and
a
cons
constructor
and
the
name
of
the
data
type,
which
is
list
underscore
VT,
which
is
going
to
be
parameterised
on
a
couple
of
things,
one
of
which
is
a
beauty
at
ype.
I
did
not
paint
this.
A
It
means
a
view,
type
of
unknown
size
and
an
int.
The
no
constructor
takes
that
thing
we
passed
in
and
zero.
This
is
a
type
level
number
zero.
Okay,
the
cons
constructor
takes
that
a
and
an
n,
which
is
an
integer
and
hands
back
the
a
Andrey
curses
on
that
list,
view
type
and
decrements
a,
and
you
can
also
provide
constraints
on
that.
So,
basically,
if
you
have
a
linear
list
of
like
one
two
three
right,
it
will
be
linear.
One
it'll
be
list.
Vt
cons,
one
list
VT.
A
Now,
let's
PT
cons,
two
lists:
PT
cons,
one
list,
VT
cons,
zero
at
the
type
level,
that's
what
it
would
look
like,
because
it's
decrementing
that
at
the
type
level,
so
here
we
have
how
you
construct
a
linear
list
list.
Vt
cons,
one
list,
VP
cons
to
list
VT
cons.
No
none
of
this
stuff
is
really
interesting.
What's
interesting
is
the
type
signature
which
is
usually
inferred
if
this
ATS
can
actually
infer
it
can
infer
precious
little,
but
it
can
infer
that
right.
A
So
it's
saying
it's
a
list
view
type
of
type
int
and
there's
two
things
inside
of
it
cool.
So
what
we're
gonna
do
is
use
that
to
make
a
factorial
that
preserves
the
results
in
a
list.
So
basically,
if
I'm
calling
factorial
10
I,
don't
just
want
factorial
10
I
want
10
times
9
10
times
9
times,
8
10
times
9
times
8
times,
7
all
the
way
down.
So
the
last
thing
in
my
list
is
going
to
be
factorial.
10
I
want
to
preserve
all
that
stuff
and
here's
the
function.
A
That
does
that
so
again,
removing
some
of
that
complexity.
The
new
concept
we
have
here
is
this
new
keyword.
Var
var
does
not
mean
what
var
means
in
every
other
language.
In
here
a
var
means
a
stack
allocated
variable
that
D
compiles
to
a
stack
allocated
variable
in
C.
That's
all
of
our
means
it
it
doesn't.
It
is
mutable,
but
it
doesn't
mean
mutable.
A
It
means
allocated,
and
here
what
we're
doing
is
saying
we're
steped
allocating
a
pointer
that
is
uninitialized,
and
then
we
have
that
function
loop
that
we
kick
off,
but
we're
returning
that
var
down
at
the
end.
So
we
have
a
factorial,
that's
parameterised
on
some
integer,
that's
modified,
so
it
always
has
to
be
greater
than
equal
to
two,
this
time,
not
greater
than
equal
to
one
I'll
get
to
that
in
a
second.
It
returns
a
list
view
type
of
a
bunch
of
doubles
where
the
length
of
the
list
is
n,
minus
1.
A
A
A
Now
this
is
the
inner
loop.
This
is
just
the
type
signature,
so,
let's
step
through
this,
so
it
takes
in
a
next
argument,
which
is
what
you
know.
What
is
the
current
index
of?
Like
you
know
the
factorial
that
I'm
on
right
now,
which
is
parameterized
by
N,
1
and
N
1,
is
an
integer
that's
greater
than
equal
to
0,
but
less
than
or
equal
to
n
minus
2
y
n
minus
2,
because
we
kicked
off
the
loop
with
I
minus
2,
right,
ok,
cool,
so
N
1
is
also
the
termination
metric.
A
You
have
to
prove
that
that
number
is
going
down
on
each
recursive
call.
It's
also
parameterised
on
that
seed,
which
is
a
double,
and
this
is
cute,
it's
parameterised
and
as
a
result,
type
and
the
ampersand
means
a
reference
to
the
question.
Mark
means
uninitialized.
So
this
means
a
reference
to
a
pointer,
that's
possibly
uninitialized,
that's
what
that's.
What
those
wanted
five
characters
mean,
and
it
transforms
that
into
a
proof.
That's
what
the
two
arrow
signs
mean.
It
keeps
getting
better,
don't
worry
it
doesn't
in.
A
Do
it
proof
that
it
is
a
list
of
view
types
of
type
double
that
is
of
length,
n,
1,
plus
1,
Y
and
1,
plus
1,
because
n
1
goes
to
n
minus
2
and
we
want
n
minus
1
because
there's
always
one
less
thing
inside
of
that
list
than
you
pass
in
and
yes,
this
is
super
confusing,
ok,
I
know
this
is
super
confusing
and
I
left.
It
super
confusing
for
a
reason,
because
I
can
hash
all
this
out
at
the
type
level.
A
These
are
exactly
the
kinds
of
things
that
go
wrong.
Imagine
all
the
tests
that
you
don't
have
to
write,
write
these
off
by
one
things
happen
all
the
time,
including
in
languages
with
really
strong
type
systems,
as
we
think
of
them,
like
Hezbollah,
like
will
have
off
by
one
type
errors.
All
of
these
things
will
have
off
by
one
type
errors.
Rust
can
have
an
off
by
one
type
error
with
refinement
types.
A
A
So
here's
the
inner
body
of
the
loop,
which
is
similarly
complicated
and
here
are
the
arguments
for
reference,
so
we're
pattern
matching
on
next.
In
the
case
of
zero
I'm,
just
setting
the
result,
the
the
the
stack
allocated
pointer,
we
passed
in
to
the
seed
and
nil.
So
if
we
off
all,
we
did
was
passed
in
two,
it
would
just
multiply
like
two
times
one
and
hand
that
back
in
a
list
for
the
next
part,
I'm
going
to
take
a
step
back
and
propose
a
puzzle
solve
this
puzzle
in
a
strict
functional
programming.
A
A
Oh,
that's,
cheating,
no
weird,
optimization!
Pragmas!
Yes,
I'm,
aware
that
there's
like
some
super
smart
compilers
out
there
that
you
can
give
like
this
magical
incantation
to
you
that
can
make
all
this
go
away.
That's
cheating
I
think
that
this
problem
is
probably
impossible.
Pick
up
pick
your
favorite,
strict,
functional
programming
language
and
look
at
the
implementation
of
map
in
it
and
see
how
it
does
it
Milton
the
standard
ml
that
is
all
about
performance
reverses.
A
So
when,
if
you
look
at
the
source
code
for
Milton's
list
map,
it
applies
a
function
to
everything
in
the
list
and
then
reverses
that
list.
So
it's
taking
two
passes
all
Camel
people's.
So
a
camel
has
this
like
mutable
accumulator,
that
it
keeps
Technion
to
the
end
of
that's
the
same
as
a
while
loop,
that's
cheating,
rust,
uses,
I
think
uses
Macker,
possibly
or
people's
one
of
the
two
or
it
just
writes
it
in
LLVM,
as
for
I,
don't
know
right,
but
until
recently
I
considered
all
of
these
things,
elegant,
hacks
and
now
I'm.
A
A
Because
you
will
never
be
able
to
port
those
ideas
to
your
day
job,
even
if
you
could
get
past
your
the
technical
hurdle
of
your
programming
language,
not
supporting
those
constructs,
you
will
never
get
there
and
you
will
be
bitter
and
unhappy.
So
you
should
all
just
leave
right
now
like,
but
if
you're
gonna
stick
around
ATS
supports
this
thing
called
tail
allocation
tail
allocation
is
was
an
idea
that
was
floated
for
ML
in
1998
and
I
learned
that
because
I
was
researching,
you
know
when
I
was
researching
ideas.
A
I
came
across
this
idea
and
it's
20
years,
and
nobody
else
has
adopted
this.
Please
adopt
this
ok.
So
what
is
tail
allocation
table
allocation
is
a
way
of
punching
a
hole
in
a
data
structure
now
punching
a
hole
that
will
be
filled
in
later
on.
In
a
way
you
can
think
of
it
as
a
principle
of
null
pointer,
but
it's
not
quite
that.
A
Now
we
have
to
actually
pattern
match
on
res
to
get
a
hold
of
that
hole,
because
ATS
doesn't
give
us
a
way
of
like
having
named
holes
on
in
one
pass.
Unfortunately,
so
that
underscore
is
that
hole,
and
then
we
calculate
the
next.
We
calculate
the
next
seed
because
we
have
to
use
that
cheesy
g0
want
to
have
function,
which
courses
from
an
integer
to
a
float
again
I
apologize,
and
then
we
call
loop
and
pass
in
that
hole
and
that's
the
hole
to
be
filled.
A
A
A
These
kinds
of
things
are
really
powerful
things
to
have,
because
functional
programming
already
has
a
reputation
for
being
slow
like
we
have
words
like
maintainable
and
stuff
like
that,
but
once
you
say,
maintainable
most
people
have
just
sort
of
already
done
like
in
C.
Programmers
don't
care
about
that.
A
Okay,
so
that
was
my
final
example,
so
here's
some
takeaways
ATS
is
rough.
There's
no
two
ways
about
it.
This
was
just
a
taste.
This
is
the
tip
of
the
iceberg,
but
it
contains
I
think
like
very
promising
glimpses.
This
would
be
if
a
bunch
of
programming
languages
took
these
ideas
and
ran
with
them.
I
think
we
would
have
a
great
systems
for
again
in
future.
Linear
logic
is
a
great
idea:
I
want
first-class
access
to
that.
Don't
don't
baby
me
away
from
linear
logic.
A
A
The
idea
of
having
a
smart
type
checker
and
a
dumb
compiler
is
great.
So
that's
what
ats
is
a
TS
as
a
front
end
to
see
that
d
compiles
into
c
code
that
you
would
have
written
in
the
first
place
or
semantically
equivalent
to
that,
and
this
idea
of
having
a
front
end
on
a
language.
That's
already
widely
used.
I
think
is
a
really
good
idea,
like
faint
type
script,
but
just
keep
going
keep
going
like
run
with
that.
A
For
like
the
next
20
years
and
see
what
happens,
I'm
forget
about
like
usability
just
run
with
it
yeah
and
there's
a
whole
bunch
of
stuff
that
I
have
even
talked
about
yet
80s
is
a
whole
proof
level
language.
It
supports
proof
by
induction
pattern,
matching
and
everything
so,
for
instance,
in
80s,
there's
this
concept
of
an
array
like
it's
the
same
as
a
CRA.
Basically
you
have
a
bank
of
proofs
that,
like
these
pointers
point
to
these
locations
and
I
can
write
a
type
level
function.
That
looks
rather
like
ml.
A
That
breaks
up
that
Bank
of
proofs
into
two
separate
proofs,
saying
that
here's
a
proof
going
from
index
1
to
5
and
here's
a
proof
coin
from
index
6
to
10.
So
the
slicing
that
other
languages
provide
as
a
built-in
is
you
can
do
it
at
the
proof
level
here
in
ATS,
because
you
have
that
kind
of
flexibility.