diff options
Diffstat (limited to 'microposts/ats.org')
| -rw-r--r-- | microposts/ats.org | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/microposts/ats.org b/microposts/ats.org new file mode 100644 index 0000000..45d6417 --- /dev/null +++ b/microposts/ats.org @@ -0,0 +1,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]] |