The ATS Programming Language

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.

I'm currently reading "The little prover". A really good book that explains this.

http://the-little-prover.github.io/

> 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).