ATS: A Programming Language That Lets You Prove Your Code Correct
Introduction to Programming in ATS
Hongwei Xi's book introduces ATS, a syntax- and feature-rich language covering functional programming, datatypes, polymorphism, dependent types, linear types, and theorem-proving. It walks through practical topics like interaction with C, modularity, and template-based programming, with worked examples from binary search trees to red-black trees. Xi warns the material is dense for readers without considerable programming experience, but no prior familiarity is assumed.
Although the reader is not assumed to be familiar with programming in general, the book is likely to be rather dense for someone without considerable programming experience.
- srean
ATS used to be discussed quite a lot on HN
https://hn.algolia.com/?query=The%20ATS%20Programming%20Lang...
MLton and Felix would be two other ML inspired languages that whole program optimizes to generate fast code.
- ddellacosta
Fun talk on this language here: https://www.youtube.com/watch?v=zt0OQb1DBko ("A (Not So Gentle) Introduction To Systems Programming In ATS" by Aditya Siram)
- drop_star
Abstract Tree Syntax