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