Programming Languages, Martials Arts and Computers. The Weblog of Chris Double.
33 posts
I wanted to look at ATS again after a long gap. I've written about it many times before but haven't done much with it in recent years. Part of what prompted this was looking at Verus for verified Rust programming and thinking about how ATS compares. ATS takes a different approach to verification. It's built into the type system itself... more →
The ATS programming language supports defining Generalized Algebraic Data Types (GADTS). They allow defining datatypes where the constructors for the datatype are explicitly defined by the programmer. This has a number of uses and I'll go through some examples in this post. GADTs are sometimes referred to as Guarded Recursive Datatypes. Some useful resources for reading up on GADTs that... more →
I've been reading the book Building High Integrity Applications with Spark to learn more about the [SPARK/Ada](https://en.wikipedia.org/wiki/SPARK_(programming_language)) language for formal verification. It's a great book that goes through lots of examples of how to do proofs in Spark. I wrote a post on Spark/Ada earlier this year and tried some of the examples in the GNAT edition. While working through... more →
This post covers using the latest version of ATS, ATS 2, and goes through proving some basic algorithms. I've written a couple of posts before on using proofs in ATS 1: more →
The ATS programming language has a powerful type and proof system to enable safe construction of programs. Sometimes there is a need to cast a value from one type to another. ATS provides a feature that enables the programming to write their own rules specifying what can be cast. This becomes important when converting types from non-dependent typed values to... more →
A few years ago I wrote a mailing list post on cross compiling ATS to Android. With ATS2 being released the ability to cross compile has been made easier. In this post I'll show how to produce static linux binaries using musl libc and how to build Android and Windows ATS programs by cross compiling on linux. For these examples... more →
Recently Robert O'Callahan wrote a post on what Rust can do that other languages can't. It involves getting a pointer to an internal field of a stack allocated object and having the type system ensure that the lifetime of that pointer doesn't outlive the owning object. As soon as I saw this I thought "Aha, ATS can do that!" but... more →
ATS is a programming language I've used a lot in the past. A new version was released a while ago, ATS2, that resulted in various library and language changes and I never got around to transitioning my code to it. Many of my existing posts on ATS are still relevant but some syntax has changed and many of my examples... more →
The Heartbleed bug in OpenSSL has resulted in a fair amount of damage across the internet. The bug itself was quite simple and is a textbook case for why programming in unsafe languages like C can be problematic. As an experiment to see if a safer systems programming language could have prevented the bug I tried rewriting the problematic function... more →
My last post that covered using proofs in ATS implemented a stack. In this post I step back a bit and go through some smaller examples using dataprop with proofs using prfun. The examples I work through here are based on the Propositions and Evidence section of Software Foundations. That book covers the Coq Proof Assistant and I've been working... more →
There's a discussion going on in the Rust mailing list about ranged integer types and whether they're useful for safety. Some of the points raised have been about the performance costs of dynamic bounds checks and the overhead of code for static bounds checks. I thought I'd write a post with my experiences with overfow checking in Gecko and with... more →
The ATS programming language was designed to enable safe systems programming. This requires dealing with pointers safely. In this post I intend to go through the basics of pointer handling in ATS and how this safety is achieved. # Raw Pointers ATS has a basic pointer type called ptr. This is a non-dependent type and is the equivalent to a... more →
This post works through an example of a stack datatype, adding ATS features as we go along to help prove the implementation is correct. The example starts with a simplified stack of integers. I then add some dependent types to improve checking of the implementation and follow this with dataprop usage for more extensive compile time checking. I use datatype... more →
In previous ATS posts I've written about how ATS can make using C functions safer by detecting violations of the C API's requirements at compile time. This post is a walkthrough of a simple example which involves a C api that copies data from a buffer of memory to one allocated by the caller. I'll start with an initial attempt... more →
I've been using libevent a fair bit recently from my systems developed in the ATS programming language. The resulting code is callback oriented and this programming style can result in difficult to follow code. Recently I ported a python programming using the twisted asynchronous network library to ATS and the callbacks were getting hard to manage. An example of the... more →
While I had some downtime travelling during my Pitcairn Island trip I made a start at writing some reference documentation for some of the ATS standard libraries. I used AsciiDoc to write the documentation because I was familiar with it from doing a reference for Wasp Lisp. I've only documented a few of the standard modules and welcome contributions for... more →
In a project I'm working on I'm using linear lists. This is the list_vt type in the ATS prelude. list_vt is similar to the list types in Lisp and functional programming languages except it is linear. The memory for the list is not managed by the garbage collector and the type system enforces the rule that only one reference to... more →
ATS has record types which are like tuples but each item is referenced via a name. They closely approximate C structs and in the generated C code are represented in this way. The following uses a record to hold x and y values representing a point on a 2D plane: fun print_point (p: @{x= int, y= int}): void = printf("%d@%d\n",... more →
ATS allows overloading of functions where the function that is called is selected based on number of arguments and the type of the arguments. The following example shows overloading based on type to provide a generic print function: symintr myprint fun myprint_integer (a: int) = printf("%d\n", @(a)) fun myprint_double (a: double) = printf("%f\n", @(a)) fun myprint_string (a: string) = printf("%s\n",... more →
While using the libevent API from ATS I came across a scenario where it was important to call a function to release objects in a particular order. I wanted to have ATS enforce at compile time that the destruction occurs safely in the right order. The following example uses the built in libevent HTTP API for creating simple web servers.... more →
My previous post on converting C programs to ATS had an example of passing a linear resource to a callback function. The code looked like: typedef evhttp_callback (t1:viewtype) = (!evhttp_request1, !t1) -<fun1> void extern fun evhttp_set_cb {a:viewtype} (http: !evhttp1, path: string, callback: evhttp_callback (a), arg: !a): int = "mac#evhttp_set_cb" ... val _ = evhttp_set_cb {event_base1} (http, "/quit", lam (req, arg)... more →
I tend to use ATS as a low level programming language - a better, safer, C. Often I start with a C program and slowly add ATS features as I go. I do this so I can utilize existing C code, write my higher level functionality in ATS, and slowly convert parts of the C to ATS to add compile... more →
A datatype in ATS is similar to types defined in languages like ML and Haskell. They are objects allocated in the heap controlled by the garbage collector. The programmer does not need to explicitly free the memory or manage the lifetime of the object. A dataviewtype is similar to a datatype in that it is an object allocated on the... more →
I'm back to using the ATS programming language after a bit of a break. My first thought upon getting back into the language is how easy it is to forget how to write in a language you don't use often. It's starting to come back to me though. For my current task I needed to read string data from a... more →
I wrote previously about using the ATS programming language to safely use C libraries. I've recently been using ATS in a couple of projects and have had to access a few more C libraries. This post goes through a few more ways ATS can be used to make it harder to incorrectly use C libraries by making some classes of... more →
Dependent types are types that depend on the values of expressions. ATS uses dependent types and in this post I hope to go through some basic usage that I've learnt as I worked my way through the documentation, examples and various papers. While learning about dependent types in ATS I used the following resources: more →
ATS uses native operating system threads for concurrency. It provides a wrapper around pthreads and a higher level API for creating worker threads and using them for parallel computation called 'parworkshop. 'parworkshop' is described in a mailing list announcement about it as: more →
While using the ATS wrapper for pthreads I noticed the use of a couple things related to closures that I hadn't seen before and therefore didn't get mentioned in my post on ATS closures. The signature for the function to spawn a closure in a thread is: fun pthread_create_detached_cloptr (f: () -<lin,cloptr1> void): void // end of [pthread_create_detached_cloptr] more →
My last post on ATS was about C style functions. This post covers what I've learnt about closures in ATS. As I mentioned in my last post, closures are functions combined with an environment mapping names to values. These are like closures in dynamic languages that enable you to capture variables in the enclosing scope. To create a closure you... more →
Using higher order functions in ATS was a bit of a struggle for me at first due to having to deal with getting types correct. I'm coming from a background of dynamically typed languages where it is easy to create and pass around anonymous functions. Even other typed languages like Haskell proved easy to pick up, primarily because of the... more →
When developing the original Ogg backend for Firefox we had to integrate and use a number of C libraries. Over the months after landing a number of bugs were raised for various issues in the backend. A fair number of these were the result of common coding errors. Things like not checking return values of the C API calls and... more →
As an exercise in learning more about ATS I worked on porting the preforking echo server I wrote in Pure. I wanted to get a feel for how higher order functions worked so I followed the same structure as the Pure program. The code I ended up with is in preforking1.dats. There is also a pretty-printed version produced by 'atsopt'.... more →
The release of Version 0.2.0 of ATS was recently announced on the ATS mailing list. From the ATS website: more →