Bug#725033: ITP: ats2-lang -- ATS (v2) is a statically typed programming language that unifies implementation with formal specification.

[Matthew Danish <mrd@debian.org>]

Package: wnpp
Severity: wishlist
Owner: Matthew Danish <mrd@debian.org>

* Package name    : ats2-lang
  Version         : 0.0.3
  Upstream Author : Hongwei Xi <hwxi@cs.bu.edu>
* URL             : http://www.ats-lang.org/
* License         : GPL
  Programming Lang: ATS, C
  Description     : ATS (v2) is a statically typed programming language that unifies implementation with formal specification.

ATS is a statically typed programming language that unifies implementation with
formal specification. It is equipped with a highly expressive type system
rooted in the framework Applied Type System, which gives the language its name.
In particular, both dependent types and linear types are available in ATS. The
current implementation of ATS (ATS/Anairiats) is written in ATS itself. It can
be as efficient as C/C++ (see The Computer Language Benchmarks Game for
concrete evidence) and supports a variety of programming paradigms that
include:

Functional programming. The core of ATS is a functional language based on eager
(aka. call-by-value) evaluation, which can also accommodate lazy (aka.
call-by-need) evaluation. The availability of linear types in ATS often makes
functional programs written in it run not only with surprisingly high
efficiency (when compared to C) but also with surprisingly small (memory)
footprint (when compared to C as well).

Imperative programming. The novel and unique approach to imperative programming
in ATS is firmly rooted in the paradigm of programming with theorem-proving.
The type system of ATS allows many features considered dangerous in other
languages (e.g., explicit pointer arithmetic and explicit memory
allocation/deallocation) to be safely supported in ATS, making ATS a viable
programming language for low-level systems programming.

Concurrent programming. ATS, equipped with a multicore-safe implementation of
garbage collection, can support multithreaded programming through the use of
pthreads. The availability of linear types for tracking and safely manipulating
resources provides an effective means to constructing reliable programs that
can take advantage of multicore architectures.

Modular programming. The module system of ATS is largely infuenced by that of
Modula-3, which is both simple and general as well as effective in supporting
large scale programming.

In addition, ATS contains a subsystem ATS/LF that supports a form of
(interactive) theorem-proving, where proofs are constructed as total functions.
With this component, ATS advocates a programmer-centric approach to program
verification that combines programming with theorem-proving in a syntactically
intertwined manner. Furthermore, this component can serve as a logical
framework for encoding deduction systems and their (meta-)properties.

ATS2 is the second major version of ATS, a complete rewrite of the compiler system.