ATS

This is a fan site about ATS, Applied Type System "unleashing the potential of types." The official ATS website is at ats-lang.org. I try to endorse ATS in my own way, but none of my endorsement is endorsed by ATS.

What do I think ATS is?

ATS is a programming language inspired by ML and C that incorporates dependent types, theorem proving, and reasoning about linear proposition. ATS is a bit similar to and can be used like:

ML, except you have to annotate types for at least the function arguments and return types (which is a good practice anyway). ATS doesn't have Hindley-Milner style type inference. ATS also doesn't have the kind of elaborated module system (structure and functor) that Standard ML has. ATS doesn't support object oriented programming like Objective CAML does. In addition, ATS doesn't have a read-eval-print loop like most functional languages have.
Dependent ML, using dependent types to help you reason about data structure integrity, from something as simple as requiring two lists to be zipped to have the same length, to preserving tree-size invariant when rotating AVL trees to the left or to the right in order to guarantee well-balanced property of AVL trees.
Theorem prover, but ATS doesn't do proof search. ATS also supports linear proposition for reasoning about resource ownership and enough flow analysis to automatically track whether resource requirements are met.
C, which offers you very fine control over memory allocation as well as the management of other kind of resources. The syntax still looks like ML, but you can do low-level programming that C can do in a much safer way. ATS also offers template, a C++ feature, though again it doesn't support object oriented programming.

When these features are combined: functional programming, dependent types, theorem proving with linear proposition, and low-level programming, you get a language that is very powerful but somewhat difficult for beginners to grasp on their own. The difficulty is further compounded by the following human factors:

Unfamiliarity with inductive reasoning and writing recursive functions. When you write a recursive function, you probably meant to write one that terminates. If you want a recursive function to terminate, you need base cases that return without making a recursive call, and inductive cases where you are sure the recursive call is only made on a smaller sub-problem (i.e. you're always making progress). A C programmer can practice this by rewriting a for-loop as a recursive function.
Incomplete understanding of the data structure model. Even an experienced ATS programmer can be confronted with a data structure he doesn't completely understand. He will have difficulty reason about his program that manipulates the data structure.
Lack of experience in writing proofs, or over-reliance on intuition. People usually make logical leaps because intuition says so. Sometimes the intuition is right. Sometimes it is not. Proofs are actually fairly mechanical and boring, but that's just the way it is supposed to be.
Lack of experience in low-level programming. After programming in Java and ML (and Obama forbids, Haskell) for a while, you forget how your programming style could generate a lot of garbage. This is probably not a problem with your favorite language since compiler optimization and garbage collectors are getting better, and computers are being equipped with more memory. But ATS forces you to think about these issues again.

ATS might not be the most elegant language, but I feel that it represents a reasonable trade-off when everything about safe and efficient programs are considered.

Articles

Here are some articles I wrote as I learned ATS. This is grossly incomplete, but hopefully that will get you started.