I came here to recommend the same video, "A (Not So Gentle) Introduction To Systems Programming In ATS" by Aditya Siram". There was probably 200-250 in the room for this talk and another 10k viewers of this video, which pretty damn cool. Some of those chuckles from the audience are mine. Thanks Aditya, Strangeloop and Hongwei Xi!
Plus for showing code. But I'm a bit confused.
Does ATS have a network library? Or a 2d canvas library ? Does it compile to JS !? I would like to see some more real life examples, maybe some simple games like tic tac toe, or a network chat server/client, or what are you supposed to use the langauge for, besides solving fibonacci ?
I wrote some things a few years ago on ATS. Its introductory but real world: https://www.stackbuilders.com/news/specific-endpoints. Generally ATS is good for verifying pure algorithms. It has code generators which can compile ATS to C and JS and the like. So if you have a very crucial piece of code and you want to do some formal verification of the process then you can try to use ATS. Other than that its completely a research language. I used ATS to write some stuff for my arduino 5 or so years ago.
Yes, "verification" in the formal verification sense of the word. https://en.wikipedia.org/wiki/Formal_verification. Also, in ATS the algorithms don't have to be "pure" in the "no stateful side effects" sense of the word to be subjected to verification. ATS is truly a nice piece of master work and hopefully its concepts can start making it out the ivory tower sooner rather than later.
How to do you verify an algorithm? Can you give me an example. Lets say you are trying to come up with some sorting algorithm, and you unknown wrote Bubble sort - how would you go about verifying the algorithm? As far as I know, we test the algorithm analytically and empirically.
Well, generally, first there has to be some things that you assume to be true - we'll call them axioms (somethings gotta be true, I mean can you prove that the natural number 0 equals the natural number 0). Then you come up with some properties about your algorithm that you want to ensure hold based on those axioms (or stuff already known to be true that are based on those axioms). So, for example, you may want to ensure that your algorithm does not change the length (or more generally the structure) of the input when sorting - e.g. if your sorted list came out with more elements than it went in with that wouldn't be sorting.
Now you don't need to have a formal proof for this right away (or at all if you don't want to really). A tool like "Quick Check" (Haskell, Erlang, ...) can help you do a quick informal check by making up a bunch of random list structures and running a unit test on all of them automatically. If your quick check property holds you may want to later try a proof and perhaps even see if something like ATS verification system is expressive enough to encode your proof or prove it for you auto style.
The benefit of the verification system is that it happens as static analysis (things that can be determined from reading the code rather than running it) the quick check stuff you need to run the code. A proof is a more complete check.
Please read the ATS (Coq, Agda, etc) stuff to learn from the experts.
> How to do you verify an algorithm? Can you give me an example. Lets say you are trying to come up with some sorting algorithm, and you unknown wrote Bubble sort - how would you go about verifying the algorithm?
Verification requires a formal specification, then we follow a fixed set of logical rules to turn the statement 'implementation XYZ matches specification ABC' into the statement 'true'. This won't always be possible: if our logic is consistent (AFAIK ATS is consistent), then it's not possible to turn the same statement into 'true' (via one sequence of rule applications) and into 'false' (via a different sequence); hence if it's possible to prove our implementation doesn't satisfy the specification (i.e. turn that statement into 'false') then it's not possible to prove that it does (i.e. turn it into 'true'). Powerful logics, like that of ATS, are also incomplete, meaning that some statements cannot be turned into 'true' or 'false'. When we write down a formal "proof" we're essentially writing down which rules to follow at each step. Note that many systems of logic, including ATS, don't quite follow the approach I just said (write down anything we want and then try to turn it into 'true', AKA 'top down proof'); instead we're only allowed to write down a series of statements that are each true, by giving a proof for each one at the point that we write it down (AKA 'bottom up proof'). In systems based on type theory, like ATS, the types act like statements their values act like proofs. Whilst type theory can help us prove statements like 'implementation XYZ matches specification ABC', we can usually abbreviate this such that the specification is the type and the implementation is the proof, i.e. 'XYZ has type ABC', where we're effectively proving the existence of a sorting algorithm by showing that we can implement one (like bubble sort).
As a side note, Kurt Gödel proved that every system of logic must be either limited (specifically, be unable to represent certain statements about arithmetic, let alone prove them), or incomplete (be unable to prove some statements true or false) or inconsistent (able to prove some statements true and false, and hence not trustworthy). This was the famous "incompleteness theorem" and was essentially the start of computer science: to prove the theorem he invented "Gödel numbering", which we would call serialising code as data; Alonzo Church had discussions with Gödel about his Lambda Calculus system (which we now call a programming language); Gödel didn't like it and invented General Recursive Functions instead, which turned out to be equivalent; Alan Turing attended a series of lectures about Gödel's work, which inspired him to write his "On Computable Numbers" paper which introduced the Universal (Turing) Machine (which we now call a computer); the reviewers of that paper recommended Turing compare his work to Lambda Calculus, which he did and found that they were also equivalent; this lead to the idea of Universal Computation (AKA Turing Completeness) and the Church-Turing thesis, that all "effective methods" of calculation can be implemented by a Turing Machine (and hence by Lambda Calculus, General Recursive Functions, or any other programming language).
End of side note.
For your example of a sorting algorithm there are a few properties we might want to specify, e.g.
- Sorting is a function from lists of some element type to lists of the same element type
- The length of the output list equals the length of the input list
- Every element of the input list is present in the output list
- Every element of the output list is present in the input list
- The output list is a permutation of the input list
- If an element 'x' appears anywhere before an element 'y' in the output list, then 'x <= y' (for some given notion of '<=')
- The number of steps taken is bounded by O(nlog(n))
We need to turn this informal* specification into a formal one, written in some formal language (like ATS). One way to do that would be formalising each bullet point and then joining them together with 'AND'; however, in this case it turn out that's overkill, since some of these properties are implied by other ones.
Specifically, if the output is a permutation of the input, then it must contain every element of the input and no others, and it must be the same length as the input, so there's not much point talking about those separately.
Likewise, if we're assuming that the given '<=' comparison defines a total order, then we don't need to prove that everything occuring before some element is <= to it. We only need to prove that the preceding element is <=, and the transitive property of '<=' ensures that the whole thing is sorted.
This leaves us with bullet point 1 (which is just a type annotation like in Java, Haskell, etc.), bullet point 5 (that the result is a permutation), bullet point 6 (which is easily proved once we've managed to prove that each element is <= its following element) and bullet point 7 (the time bound).
There's a nice blog post which proves all of these for merge sort at https://www.twanvl.nl/blog/agda/sorting and a similar thing can be done in ATS (with the slight complication that, unlike Agda, ATS uses separate namespaces for runnable-parts-of-the-program and compile-time-proof-stuff).
There are some libraries for ATS, but it's not a well known language so there is not too many out there. ATS makes it easy to mix C by embedding it within ATS, and defining an interface that makes it harder to unsafely use the C API. Since it's so easy most people probably just do this when they need a C library.
There are wrappers for libevent which I've used for the network side of long running server side programs in ATS in this manner.
With regards to "Does it compile to JS", the answer is yes. There are backends for different languages, JS being one of them. There's also PHP and Erlang backends IIRC.
ATS did beat C++ in the benchmark game. Plus it's a much safer language, with proper contracts and a proper typesystem. It's more comparable to ADA/Spark (just a more C like syntax, not Pascal), than Coq/Agda or any JS based language.
It's misleading. ATS is basically a C frontend. If you looked at the ATS implementations in the benchmarks game, it was basically C code. The C implementations usually beat the C++ implementations in the benchmarks game.
The front page doesn’t do a great job of describing such details. It is a language for systems programming and compiled to fast C. The main idea is that it is supposed to compile to correct C.
I’ve no idea if it has a “native” network library. I doubt it has many other libraries but one can call C functions so one can use any library if one wants.
Having to use C libraries for critical stuff like networking (just application-level protocols, like http, not drivers) defeats some of the purpose of provable correctness, etc.
I feel like this kind of intensely provably-correct language (this one, Coq, Agda, etc.) isn't so much for writing whole programs in, as for writing the small, very-important-to-verify modules, that will link with other, less important modules to form a whole program.
When you're writing provably-correct "error kernels"[1] for your software, you probably want as little interaction with the OS to happen inside the kernel as possible. Write the rest of your program in a glue language, then hand off to the proven-correct error kernel for the hot loop. Probably over stdio, or transactional SHM IPC, or any other mechanism like that that has as little failure-surface as you can get away with.
ATS enables declaring the interface to C libraries to a very detailed level for proving. It can make using C libraries more safe than using them from C, once defined. Here is an example I wrote about how to make calling a C library safer from ATS https://bluishcoder.co.nz/2012/08/30/safer-handling-of-c-mem...
It does but without it you have a chicken / egg situation where developers wouldn't use ATS without the library support but those libraries don't get written without developers using ATS.
At least this breaks the deadlock and in the future those libraries might be replaced with ATS alternatives.
Rome isn't built or rebuilt in one day though. Just as in the case of Mozilla with Rust, interoperability with C means there is a path for migrating to a safer world.
> Does ATS have a network library? Or a 2d canvas library ? Does it compile to JS !? I
It's pretty easy to use C code for libraries.
I haven't use the ATS -> JS compiler myself but I know it exists. Though given that ATS was designed for kernel programming, I'm not sure you'd want to do that.
> I would like to see some more real life examples
There are some very nice examples, though they tend to be lower-level so things like type-safe channels.
Indeed. Quick googling around did not bring me any satisfactory answer. http://www.ats-lang.org/Libraries.html shows that batteries are definitely not included, at least yet.
I first learned about ATS when it came out on the top (2nd, 3rd?) of the benchmark game. That was years ago. Did it gain any real world traction in the meantime? It seems ATS was removed from the benchmark game since then.
I was impressed with its speed, but then I found that the reason ATS is so fast was that you basically just write C code in it to get it be fast. It's pointless to benchmark as a language of its own.
It has a backend via C and thus GCC, but it enables some things that plain C doesn't due to making certain things easier, plus the ABI for functional programming stuff matches up very cleanly with the hyper-optimized stuff.
