Highly recommended watching this before you dive into ATS
I think it's accidentally truncated, the full video id here: https://youtu.be/zt0OQb1DBko
Could you please elaborate on that?
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.
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 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.
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.
That's probably why it got removed.
The story that icc generates faster code has been a myth for a long time.
Or is there another compiler that you have in mind?
Many HPC centers happen to believe on the icc myth.
Although my point was not to mix languages with implementations.
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.
When you're writing provably-correct "error kernels" 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.
At least this breaks the deadlock and in the future those libraries might be replaced with ATS alternatives.
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.
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.
Still a research language, but pretty fun.