Spinroot

Google Group
1

hello,
Did you ever see this project : http://spinroot.com/

For a newbie in dependent types, I would say it is similar to ATS goals of
software verification.

What is different from ATS ?

2

A program is like a big company with many workers. Dependent types can be
used to precisely describe the task each worker should perform. Linear
types can be used to track the resources inside the company (e.g. copy
machine). The type checker of ATS can verify individually that each worker
can finish the task if he or she sticks to the declared working plan
(code). But such verification only makes sense when all of workers can get
exclusive control of resources they want. The working plan is encode in ATS
as well as the proof that such plan works. The type checker only checks
whether the proof makes sense. The good thing is that the verification can
be done ahead of the time that the company opens and the task described can
be very complicated and in an unlimited scale.

3

maybe spin look for exploring paths from non-deterministic code and show
some quirks. It is very concurrency oriented.

and I see ATS more as producing semantic proved programs
I did not look yet in multi-threads example in ATS. Does dependent types
can help preventing dead-lock or race conditions ?

My feeling is that linear types can help a lot for that kind of problems…

4

Yes, we are interested in SPIN, too.

However, what ATS tries to accomplish is different from SPIN.

Often people think that program verification means verifying the
correctness of
a given program. But how do you get the program to verify in the first
place? ATS tries
to accommodate a way of program development in which program verification
is combined with program construction. I think this is key to program
verification
being actually used in practice. So first and foremost, ATS tries to be a
language
that can help people write programs, any programs.

5

Linear types allow you to track resources. However, without dependent
types, we don’t get enough precision.
So what we really need is linear dependent types.