aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYuchen Pei <me@ypei.me>2018-05-22 12:43:44 +0200
committerYuchen Pei <me@ypei.me>2018-05-22 12:43:44 +0200
commitfdbffaff7615139e81eadd08659d7ed9a46c28c8 (patch)
treeda65c3ff6a8457c1fd5bcecbd4826a46880fab62
parent7a6a41cf53b1684f4e1da430c2873323be1a1557 (diff)
added a micropost
-rw-r--r--microposts/ats.md7
1 files changed, 7 insertions, 0 deletions
diff --git a/microposts/ats.md b/microposts/ats.md
new file mode 100644
index 0000000..867ce88
--- /dev/null
+++ b/microposts/ats.md
@@ -0,0 +1,7 @@
+---
+date: 2018-05-22
+---
+
+> 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.[2] 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.
+
+[Wikipedia entry on ATS](https://en.wikipedia.org/wiki/ATS_(programming_language))