blob: 45d64174a14c83ba81b5a829bb20216d18d0d520 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
#+title: ats
#+date: <2018-05-22>
#+begin_quote
ATS (Applied Type System) is a programming language designed to unify
programming with formal specification. ATS has support for combining
theorem proving with practical programming through the use of advanced
type systems. A past version of The Computer Language Benchmarks Game
has demonstrated that the performance of ATS is comparable to that of
the C and C++ programming languages. By using theorem proving and
strict type checking, the compiler can detect and prove that its
implemented functions are not susceptible to bugs such as division by
zero, memory leaks, buffer overflow, and other forms of memory
corruption by verifying pointer arithmetic and reference counting
before the program compiles. Additionally, by using the integrated
theorem-proving system of ATS (ATS/LF), the programmer may make use of
static constructs that are intertwined with the operative code to
prove that a function attains its specification.
#+end_quote
[[https://en.wikipedia.org/wiki/ATS_(programming_language)][Wikipedia
entry on ATS]]
|
