Many thanks to jns for the -w 76 smart formatting!
---
I don't know if you watched Austin Powers 2, but his self-published book
captures my relationship with formality. It has been a while since I have
thought logically at all, so I went for insertion sort in acl2 which was
remembered to me. In acl2 we are not able to do this:
```sbcl
(sort '(3 4 1) '<=)
```
>(1 3 4)
which is informal. Informal means that we know what the word sort means, and
it is in the function position of a lisp list, and it is being passed a data
list and a symbol that obviously names a comparison predicate, and our
brains fill in what is intended based on our experience, including a handful
of algorithms. I will do a formal insertion sort for '<= here now too.
Insertion sort goes stepwise like this (very informally):
'((input . (3 4 1)) (ouput . ()))
'((input . (4 1)) (ouput . (3)))
'((input . (1)) (ouput . (3 4)))
'((input . ()) (ouput . (1 3 4)))
; the right side is always in order, so it is easy to move the 'car on the
left to its right position on the right. Formal methods is similar to
testing, sofaras alternatives are similar. Instead of checking for problems
you have seen come up before or can imagine (testing/informality), you prove
a hopefully accurate model of your system up from completely accepted axioms
like a few properties of the cardinal numbers (with a robot teammate who can
do string searches much quicker than you). Less talking, more easy codes:
** Insertion sort
*** A comparison
```acl2
(defun leq-pushp (a b)
(if (<= a (car b)) (append (list a) b)
nil))
```
Admitted trivially; the function is a nonrecursive if statement, returning
some non-nil useful data or else nil (indicating failure).
*** Sorted insertion
```acl2
(defun insert-sorted (a b result)
(if (= 0 (length b)) (append result (list a))
(let ((final-tail (leq-pushp a b)))
(if final-tail (append result final-tail)
(insert-sorted a (cdr b) (append result (list (car b))))))))
```
To find where a fits into b, values at the front of b get moved one by one
into a result list. Once a is not greater than the front of b, we return a
sorted result (tail recursively, so far as speed matters here...!). The
measure is the length of b, which always decreases (and is terminating if it
reaches 0). This lets our robot teammate easily figure out that the
function's recursion is progressing towards a result.
*** Insertion sort
```acl2
(defun insertion-sort (input result)
(if (= 0 (length input)) result
(insertion-sort (cdr input)
(insert-sorted (car input) result nil))))
```
Tail-recursively insert-sorted the front value of input into a result list.
The measure is that the length of the input counts down to 0.
*** Proving something
Aside: #'search returns nil or the index of where the first argument starts
within the second argument indexed from 0.
```acl2
(thm (implies (< a b)
(< (search (list a) (insertion-sort (list a b 3) nil))
2)))
```
**** Informally
If the variable a is less than the variable b then a cannot possibly be the
last element of (insertion-sort (list a b 3) nil). The last element
(position 2, indexed from 0) must be the value of b or 3. Just because it
comes up in a moment I note here that acl2's formal search permits either
two lists or two strings, which I guess is why our robot friend collected
(:DEFINITION STRING-DOWNCASE).
