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

**** Formally, though!
<many lines omitted>

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION BINARY-APPEND)
        (:DEFINITION INSERT-SORTED)
        (:DEFINITION INSERTION-SORT)
        (:DEFINITION LEN)
        (:DEFINITION LENGTH)
        (:DEFINITION LEQ-PUSHP)
        (:DEFINITION MV-NTH)
        (:DEFINITION NOT)
        (:DEFINITION NTHCDR)
        (:DEFINITION SEARCH-FN)
        (:DEFINITION SEARCH-FROM-START)
        (:DEFINITION STRING-DOWNCASE)
        (:DEFINITION SUBSEQ)
        (:DEFINITION SUBSEQ-LIST)
        (:DEFINITION TAKE)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART BINARY-APPEND)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART LEN)
        (:EXECUTABLE-COUNTERPART LENGTH)
        (:EXECUTABLE-COUNTERPART TAKE)
        (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
        (:EXECUTABLE-COUNTERPART UNARY--)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE CONS-EQUAL))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION BINARY-APPEND)
             (:DEFINITION INSERT-SORTED)
             (:DEFINITION INSERTION-SORT)
             (:DEFINITION LEQ-PUSHP)
             (:DEFINITION SEARCH-FN))
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
Prover steps counted:  3180

Proof succeeded.