Talk:ATS: Programming with Theorem-Proving
Add topicThis book is about the ATS programming language system. WIKIBKhwxi (talk) 18:10, 8 December 2010 (UTC)
The page Using Wikibooks/How To Structure A Wikibook has a recommendation to make a plan for a book up-front, so I'll try to summarize who is this book going to be for, and outline its overall structure. If you find any of this incomplete or unsound, please do not hesitate to discuss your thoughts.
The intended audience is programmers having experience with
- structured, procedural programming using type-safe and unsafe languages (Pascal, C/C++)
- functional programming using descendants of ML (SML and OCaml mainly, and Haskell to a smaller extent)
So this book isn't intended teach you when to use abstractions and how to derive them, why modular code is superior to monolithic code (in many cases) and others questions in this vein -- these questions are to be explored elsewhere. I'd like to concentrate on the actual usage of the language for doing various tasks (as Matthias Felleisen put it, "to count sheep").
The book should cover these broad topics:
- informal syntax and operational semantics of ATS (I don't think we need to be very precise here, i.e. no formal models, just description of what individual parts of programs do and what happens when they are combined)
- discussion of types and programs, propositions and proofs, and formal specifications (not very pragmatic, I know -- at least not directly applicable -- but should ease understanding of use of type system in ATS)
Here's the proposed outline (somewhat influenced by "Functional Programming in CLEAN", P. Koopman et al):
- Preface
- Purely functional programming
- Constants, arithmetic and functions
- Data structures
- I/O and imperative programming
- Types
- Why types? (a little bit of theory about type safety and related things)
- Singleton and dependent types
- Views and viewtypes
- Programming with theorem proving
- Formalizing deductive systems
- Explicit resource management
(we go from least complicated to most complicated things: "calculator" evolves into a language with support for functional, imperative and typeful programming)
Preface is meant to clearly state to the audience what they should (and should not) expect of the book.
Introduction to functional programming is given in the first chapter: we are to treat the basic aspects of programming in ATS (functions, data structures, I/O and type-system). The idea is to allow readers to write simple functions and applications as soon as possible, and there is no intention to treat all available features, but only the most important ones (the most commonly used). In contrast to books on other ML-derivatives, we will have to cover types more thoroughly. A complete description of said features is to be left to the manual.
It would be nice, I suppose, to make the book as linear as possible: every term or notion introduced only depends on those introduced before.