In his blog post "Verified software can (and will) be cheaper than buggy stuff" Gernot Heiser argues that in the future it will be cheaper to formally verify software, including, not limited to, but especially the highassurance stuff, than to deploy buggy, unverified versions of it; and since we're talking about highassurance software, this would be taking into account the risks of critical bugs occurring and the costs involved^{1}. To quote:
Our paper describing the complete seL4 verification story analysed the cost of designing, implementing and proving the implementation correctness of seL4. We found that the total cost (not counting oneoff investments into tools and proof libraries) came to less than $400 per line of code (LOC).
[...]
Another data point is a number quoted by Green Hills some ten years ago: They estimated the full (design, implementation, validation, evaluation and certification) cost of their highassurance microkernel to be in the order of $1k/LOC.
In other words, we are already much cheaper than traditional highassurance software, and a factor of 23 away from lowassurance software. If we could close the latter gap, then there would be no more excuse for not verifying software.
I have a lot of respect for Heiser and his crazy idea of driving microkernels^{2} towards full correctness. I will however leave aside the appeal to authority that he's a great researcher and I'm mostly nobody, and note that I am completely at odds with the dollars per LOC metric for measuring costs. This seems like a computed average value, which I am not convinced has too much relevance in general, falling in the same category as the manhour metric.
We do know that seL4 has about 9000 LOC, which brings us to about 3 million and a half dollars total costs, not counting tools and proof libraries. This may not be much of a cost for DARPA, but it does mean a lot of resources for the average guy who wants to make a business in this world. Also, to twist the knife a bit, tools and proof libraries add to what I call "the problem of trust"^{3}.
In this context, the problem of trust instantiates to the fact that some  maybe most  software is written in a highlevel programming language, which brings the need of translation of highlevel code to machine code using a compiler. To achieve full system verification we need to verify the compiler itself, which has been done by partially modeling said highlevel language in the higherlevel language of a proof assistant. The proof assistant ensures that the proof is mechanically sound, but the proof assistant itself is not safe from bugs, which reduces our problem to at least one of GĂ¶del's incompleteness theorems.
This brings into discussion the following question: given a fair amount of mathematical skill, can a fairly skilled engineer verify the correctness of a fairlysized system while placing a minimal amount of trust in assistance tools? Or, in other words, assuming that the tools are only there to assist, not to replace, can the engineer be provided with extra value while actually reading the code and working to understand the system^{4}?
I tend to think that Heiser's Cogent approach, a followup of the seL4 work, is useless. Looking at the Cogent git repository, it seems like a huge tool requiring a considerable amount of computational resources, while providing no extra help in making the system more palatable to our fairly skilled engineer. In fact it makes it less palatable by requiring the engineer to also understand Cogent, or give our engineer the option of viewing Cogent as a blackbox, which beats the purpose of its open sourceness.
But instead of stating empty accusations, let us try to verify a small piece of software which is a potential part of any system, so it could be included in a socalled proof library^{5}. This marks the beginning of a very long text, so grab some coffee, a pen and a piece of paper and brace yourself. We will specify a common data type in most languages, lists, and formally verify a small part of their properties. Formal verification of a piece of software requires firstly a representation of that software, and secondly a model of execution for it.
Note that while we will use a formal language for this purpose, we will not employ any proof assistant to aid us, but instead we will rely completely on the power of our intellect.
The list abstract data type, and two operations over lists
In computer science, lists are typically defined as:
List ::= []  Value : List
The formal language used to define lists is very similar to the
BackusNaur Form: ::=
means "is", so List
is a data type and []
and Value : List
are potential values of that data type. []
and :
are the two constructors of values of the type List
: []
denotes the
empty list, while x : L
denotes a value x
prepended to a list L
using the :
operator. So the list [1, 2, 3, 4]
can be represented in
our language as
1 : (2 : (3 : (4 : [])))
with the parentheses used to make associativity explicit. For the sake
of readability we will consider that :
is rightassociative, so the
previouslydefined list can also be written as
1 : 2 : 3 : 4 : []
To keep things short, let's assume our language allows us to define
functions such as f(x) = x
, and functions of multiple parameters such
as g(x,y) = x : y : []
. Also, let us assume that Value
s can be
anything; I used the symbols 1
, 2
, 3
and 4
previously, but they
can be anything we want.
Again, for the sake of brevity, we will assume that the computational
execution model of our language is simple substitution, under an
arbitrary order. So, reusing our previous examples, f(2)
and 2
are
equivalent under substitution, and so are g(1,jabberwocky)
and 1 :
jabberwocky : []
.
Equipped with this knowledge we may now define two operations on lists:
concatenation (or "append"), which we will denote app
, and reversal,
which we will denote rev
. Note that these are both the definitions
and specifications of the operations. We may informally state that
"reversing a given list yields the list which has the same elements but
in the exact opposite order (e.g. righttoleft, as opposed to
lefttoright)", but we have no way of accurately specifying this in
our language other than by defining rev
and postulating that "rev
reverses any given list". The same goes for appending lists.
I will mark the definitions' names in parentheses, as follows:
app([] , L2) = L2 (a1)
app(x : L1, L2) = x : app(L1, L2) (a2)
There are two interesting things to note here. One is that we use
substitution to pattern match app
's arguments; by definition there
are only two potential types of values that any list can take, []
and
x : L1
. The second observation is that under substitution, any
application of app
on two finite lists^{6} is guaranteed to
terminate. This second property can be proven, but the demonstration
falls out of the scope of this essay.
We will use app
to define rev
the following way: reversing an empty
list yields an empty list; reversing a nonempty list is equivalent to
app
ing the head of the list to the reversal of the rest of the list:
rev([]) = [] (r1)
rev(x : L) = app(rev(L), x : []) (r2)
So, this is it, the implementation of the two functions. It's pretty simple and it can be implemented almost adliteram in most of the commonly known programming languages. In socalled "functional languages" we get these implementations almost for free.
List reversal is involutive, the shortest proof I could muster
Reversal has an interesting property, namely that any list reversed
twice yields the initial list. This is called involution, and we will
define it for rev
as a theorem:
Theorem (T1). rev
is involutive, i.e., for any list L
,
rev(rev(L)) == L
where ==
denotes structural and valuewise equivalence^{7}.
Let's try to demonstrate this. We will do this by deconstructing L
into all possible values. Since :
is defined recursively, we will use
structural induction  which is very similar to the mathematical
induction taught in highschool  to prove that the property holds. So
we have two cases:
T1. a. For L = []
, this can be proven by applying substitution
under r1
twice:
rev(rev([])) == []
r1
rev([]) == []
r1
[] == []
T1. b. For L = x : L'
, where L'
is an arbitrary list, we assume
by induction that rev(rev(L')) = L'
. Hopefully we will get to a form
where we can apply this substitution and obtain trivial equivalence:
rev(rev(x : L')) == x : L'
r2
rev(app(rev(L'), x : [])) == x : L'
At this point we're pretty much stuck. One option would be to
deconstruct L'
and hope we get somewhere, but I'm willing to bet that
would get us nowhere. We're not left with much besides that. The astute
computer scientist will observe that we're applying rev
on an app
,
which is supposed to tell something. The even more astute computer
scientist will observe that there must be a relation between rev
and
app
^{8}.
More precisely, reversing an append between two lists should also yield an append form, but between the two lists reversed, with the arguments to the append reversed. Let's stop for a moment and write this as a lemma.
Lemma (L1). Given two lists L1
and L2
, the following is
always true:
rev(app(L1, L2)) == app(rev(L2), rev(L1))
which is quite intuitive, if we think of it. Let's try to prove
this. Since app
's recursion is done on the first argument, our best
bet is to try and deconstruct L1
.
L1. a. L1 = []
. This is pretty easy, as we can intuitively
substitute under definitions a1
and r1
:
rev(app([], L2)) == app(rev(L2), rev([]))
a1 r1
rev(L2) == app(rev(L2), [])
and we're stuck again; but we notice that the right hand of our equation is pretty trivial by nature. We already know by definition that concatenating an empty list and a list yields the latter, but we also need to prove that concatenating a list and an empty list yields the former. That is:
Lemma (L2). Appending an empty list to a list L1
will yield
L1
, i.e.:
app(L1, []) == L1
The proof should be straightforward, by deconstructing L1
.
L2. a. L1 = []
app([], []) == []
a1
[] == []
L2. b. L1 = x : L1'
, where we assume by induction that app(L1',
[]) == L1'
.
app(x : L1', []) == x : L1'
a2
x : app(L1', []) == x : L1'
ind_L2b
x : L1' == x : L1'
So, we've finally proven something! Let's get back to L1. a.. We
know that our L1 = []
and we're left with proving that:
rev(L2) == app(rev(L2), [])
L2
rev(L2) == rev(L2)
We're now left with one case for Lemma 1.
L1. b. L1 = x : L1'
, where we assume by induction that given a
list L2, we have following relation:
rev(app(L1', L2)) == app(rev(L2), rev(L1')) (ind_L1b)
We try to go the straightforward way:
rev(app(x : L1', L2)) == app(rev(L2), rev(x : L1'))
a2 r2
rev(x : app(L1', L2)) == app(rev(L2), app(rev(L1'), x : []))
r2
app(rev(app(L1', L2)), x : []) == app(rev(L2), app(rev(L1'), x : []))
ind_L1b
app(app(rev(L2), rev(L1')), x : []) ==
app(rev(L2), app(rev(L1'), x : []))
We're stuck again, but we trivially observe that what we need to prove
is that app
is associative.
Lemma (L3). app
is associative, i.e., given three lists
L1
, L2
and L3
, we have:
app(app(L1, L2), L3) == app(L1, app(L2, L3))
which we will try to prove by deconstucting L1
.
L3. a. L1 = []
, gives us
app(app([], L2), L3) == app([], app(L2, L3))
a1 a1
app(L2, L3) == app(L2, L3)
L3. b. L1 = x : L1'
, assuming that
app(app(L1', L2), L3) == app(L1', app(L2, L3)) (ind_L3b)
we reason that:
app(app(x : L1', L2), L3) == app(x : L1', app(L2, L3))
a2 a2
app(x : app(L1', L2), L3) == x : app(L1', app(L2, L3))
a2 ind_L3b
x : app(app(L1', L2), L3) == x : app(app(L1', L2), L3)
Now we can return to L1. b. (again!). We had to prove that:
app(app(rev(L2), rev(L1')), x : []) ==
app(rev(L2), app(rev(L1'), x : []))
which can be trivially proven using Lemma 3.
Long story short, we need two ancillary lemmas to prove one lemma that hopefully will help us prove Theorem 1. But before that, let's prove another simple lemma, which, as we will see, will also be of help.
Lemma (L4). Reversing a singleton list is reflexive, i.e.
rev(x : []) == x : []
We apply r2
and we obtain:
app(rev([]), x : []) == x : []
r1
app([], x : []) == x : []
a1
x : [] == x : []
Finally, T1. b. We assumed that rev(rev(L')) = L'
and we have to
prove that:
rev(app(rev(L'), x : [])) == x : L'
L1
app(rev(x : []), rev(rev(L'))) == x : L'
L4 ind_T1
app(x : [], L') == x : L'
a2
x : app([], L') == x : L'
a1
x : L' == x : L'
Thus we have, after a bit of effort, proved a property of list reversal, but in the process we managed to prove other things, such as the associativity of concatenation and the reflexivity of reverse applied on singleton lists. This however is far from the entire story.
An alternate definition of rev
, and a proof of equivalence
In addition to proving properties about programs, it is often required of socalled "proof engineers"^{9} to prove that two programs are equivalent. This is equivalent to showing that for all the inputs of a program, the outputs are exactly the same, but in fact it isn't as simple as it sounds, as both the input space, the output space and the internal state of a program  which must be somehow exposed in the specification  can be too large to simply enumerate.
Consider for example the problem of proving that for a given natural
number n
, the sum of all the numbers up to n
equals (n * (n +
1))/2
, which is the same as proving that the former sum and the latter
formula compute the same thing. This is easy enough to prove
mathematically, but it's not trivial to show using an axiomatic formal
system. Some questions that will inevitably arise is,
what is a number and how can it be represented? What do +
,
*
and /
mean? What are the properties of all these operations? And
so on and so forth.
Proofs of equivalence may also be necessary in order to show that a
program implemented in two programming languages "does the same thing"
in both implementations, at least in some respects. This is the case
with seL4 being initially implemented in Haskell, then in C, which
required a proof that the C implementation "does the same things" as the
Haskell one. We will show that it is also useful for our simple rev
example.
Our rev
implementation, which, as we said, is also our formal
specification for list reversal, suffers from one serious issue. Since
it appends values to the end of the list, its worst case computational
complexity is O(n^2)
^{10}. However the same functionality can be
implemented as a function running in O(n)
, which for functional
languages also provides other practical advantages such as optimization
of tail recursion.
The implementation is also simple: if we take the elements in a given
list L
one by one and we put them in another list using :
, then
eventually we will be left without elements in the first list, and the
second list will contain the initial elements in the reversed
order. Let's define a function called rev'
that has an additional
parameter used exactly for this purpose:
rev'([] , A) = A (r3)
rev'(x : L, A) = rev'(L, x : A) (r4)
Note that this is not immediately intuitive, as we must give A
a
specific value when we call rev'
. We can give a simple example of
evaluation by substitution:
rev'(1 : 2 : 3 : [], A) =(r4) rev'(2 : 3 : [], 1 : A) =(r4)
rev'(3 : [], 2 : 1 : A) =(r4) rev'([], 3 : 2 : 1 : A) =(r3)
3 : 2 : 1 : A
so in order to reverse a list L
using rev'
, all the calls to it must
have the form rev'(L, [])
^{11}.
We have shown through a simple example that rev'
does the same thing
as rev
, but given our neat formal language, we can actually put this
in the form of a theorem:
Theorem (T2). Given a list L
,
rev(L) == rev'(L, [])
As before, the sane approach to proving this is to deconstruct L
.
T2. a. L = []
, thus
rev([]) == rev'([], [])
r1 r3
[] == []
T2. b. L = x : L'
, assuming the induction hypothesis rev(L') ==
rev'(L', [])
. We get:
rev(x : L') == rev'(x : L', [])
r2 r4
app(rev(L'), x : []) == rev'(L', x : [])
Expectedly, we are stuck. None of the properties we know (including the
induction hypothesis) seem to help, and deconstructing L'
might bring
us to a uselessly infinite loop. Looking at this deeply  and
unfortunately we cannot escape this leap in logic  the astutest
computer scientist can figure out that, given two lists L1
and L2
,
there is some sort of link between app(L1, L2)
and rev'(L1, L2)
. The
former takes elements from L1
and puts them into L2
from right to
left, while the latter does the same, only from left to
right^{12}. So the place where we're stuck in Theorem 2 reveals a
deeper property, which we will put in the form of a lemma.
Lemma (L5). Given two lists, L1
and L2
, the following holds:
app(rev(L1), L2) == rev'(L1, L2)
We use the same pattern of reasoning as before:
L5. a. L1 = []
, thus
app(rev([]), L2) == rev'([], L2)
r1 r3
app([], L2) == L2
a1
L2 == L2
L5. b. L1 = x : L1'
, assuming that given an L2
list,
app(rev(L1'), L2) == rev'(L1', L2) (ind_L5b)
then
app(rev(x : L1'), L2) == rev'(x : L1', L2)
r2 r4
app(app(rev(L1'), x : []), L2) == rev'(L1', x : L2)
We're stuck yet again, but the right hand side of the equation provides
us with a hint that is not immediately intuitive. We have rev'(L1', x :
L2)
, which is similar to the one in the induction hypothesis, only the
second argument of rev'
has a different value. I haven't gone into the
logical bowels of this problem until now, but notice that the induction
hypothesis holds for all L2
, not necessarily the L2
in the
equation. In other words, L2
is universally quantified in the
induction hypothesis^{13}!
Thus we can instantiate L2
in ind_L5b
to x : L2
, turning this
into:
app(app(rev(L1'), x : []), L2) == app(rev(L1'), x : L2)
This is a more general statement to prove, so let's put it in its own lemma.
Lemma (L6). Given two lists L1
and L2
, concatenating
app(L1, x : [])
and L2
is the same as concatenating L1
and x :
L2
.
app(app(L1, x : []), L2) == app(L1, x : L2)
We deconstruct L1
, as usual:
L6. a. L1 = []
app(app([], x : []), L2) == app([], x : L2)
a1 a1
app(x : [], L2) == x : L2
a2
x : app([], L2) == x : L2
a1
x : L2 == x : L2
L6. b. L1 = y : L1'
, with the induction hypothesis that given a
list L2
,
app(app(L1', x : []), L2) == app(L1', x : L2) (ind_L6b)
Our reasoning goes:
app(app(y : L1', x : []), L2) == app(y : L1', x : L2)
a2 a2
app(y : app(L1', x : []), L2) == y : app(L1', x : L2)
a2
y : app(app(L1', x : []), L2) == y : app(L1', x : L2)
ind_L6b
y : app(L1', x : L2) == y : app(L1', x : L2)
Note that Lemma 6 is a very neat simplification rule that we can use back in Lemma 5:
L5. b.
forall L2. app(rev(L1'), L2) == rev'(L1', L2) (ind_L5b)
app(app(rev(L1'), x : []), L2) == rev'(L1', x : L2)
L6
app(rev(L1'), x : L2) == rev'(L1', x : L2)
ind_L5b(L2=x : L2)
rev'(L1', x : L2) == rev'(L1', x : L2)
Now that we've finally proven Lemma 5, we can move back to Theorem 2:
T2. b. Assuming the same induction hypothesis (that isn't useful here anyway), we apply Lemma 5, yielding:
app(rev(L'), x : []) == rev'(L', x : [])
L5
rev'(L', x : []) == rev'(L', x : [])
Thus we have the full proof that the two rev
functions are
equivalent. As an observation, this isn't mindnumbingly difficult, but
it can take something up to two hours for a fairly skilled engineer to
grok this^{14}. Given a proof assistant with which the fairly skilled
engineer is not necessarily acquainted, it can take more than that.
Given that we can make decent leaps in logic which won't hurt the
overall reasoning, while something such as Isabelle/HOL has its own
peculiar constructs that require some training even for the experienced
programmer, I'd say that our mindbased adhoc concocted formalism wins
hands down.
Concluding remarks
A good exercise for the aspiring software proof engineer is to imagine (and exercise) how this approach scales up to a full system^{15}. For real software the biggest part of this work goes into the brainwreckage that is correct specification within the formalism: some formalization of the C language might not like the way one uses pointers, so entire data structures have to be rethought in order for the proof to continue. For other parts the engineers might just have to assume correctness  what if the hardware has bugs^{16}? what if the compiler generates broken code? what if the language runtime has bugs? Haskell runs on glibc, which... well.
Another thing to consider is that realworld highassurance systems
usually run on imperative languages such as wellspecified subsets of
C. But for the sake of fun let's take (Common) Lisp, which has been my
favourite language for a while. I will give a Lisp implementation of
rev'
, which I name revacc
:
> (defun revacc (L A)
(if (null L)
A
(revacc (cdr L) (cons (car L) A))))
REVACC
> (revacc '(1 2 3) '())
(3 2 1)
This implementation can be further optimized into an equivalent
imperative (and uglier) implementation, which I will name revimp
. I
will use the do
macro to do this:
> (defun revimp (L A)
(do ((x (pop L) (pop L)))
((null L) (push x A))
(push x A))
A)
> (revimp '(1 2 3 4) '())
(4 3 2 1)
The Lisp family has the advantage that the core language is very well
specified^{17} and its execution model is surprisingly easy to
understand. Even so, imperative programs are not inherently simple to
formalize, since they incur the notions of time, execution steps and
program state, requiring specific operational semantics. Once these are
defined, one can formally verify that revimp
and revacc
(or
revimp
and a Lisp implementation of rev
) are equivalent, although
this is nowhere near trivial.
Coming from a formal methods dilettante and a computer scientist and engineer^{18}, the conclusion to this essay is somewhat selfevident: formal methods are good as mental exercise and a nice tool for learning; maybe a nice tool for intellectual wankery, at least in software. But cheaper than software that doesn't suck? And for all the others, bugs, a thing of the past? I very much doubt that.

These are generally hard to estimate, but we can consider examples such as the Challenger disaster, Ariane 5, hardware bugs such as Intel's FDIV bug and so on. Analyzing the causes and the costs behind all these might make an interesting exercise, but maybe for another time. ↩

I discussed them very briefly in the past, mentioning that operating system design is in fact plagued by a more general problem that is not entirely solved by microkernels and is generally ignored by the engineering and scientific community. In other words, it seems that UNIX has become "enough for everybody" and there are small chances of this changing in the current culture. Maybe in the next one, who knows. ↩

I promise to detail this in a future essay. In short, the problem's statement is that outsourcing trust in a component of the system does not magically remove the potential problems arising from said component, and that this issue goes "turtles all the way down" to the wheel and the fire, or to the fabric of the universe, if you will. ↩

I'm not even questioning whether reading the code and understanding the system is worth the engineer's time. A fair understanding of the system is an imperative prerequisite, any questioning of this being not only silly, but downright antiintellectual. ↩

Yes, library code requires reading and understanding as well! No sane person ever went to the library to grab a piece of text and use it without reading it beforehand. ↩

We have no concept of "nonfinite lists" in our language anyway. ↩

Without getting into gory details, structural equivalence means that for our abstract data type, two values of the form
a : b : c : []
andd : f : e : []
are the same, whereasa : b : []
andd : f : e : []
are different. Valuewise equivalence denotes that two arbitrary values of the typeValue
are the same, i.e.jabberwocky == jabberwocky
. ↩ 
Very much related to the fact that
app
is a free monoid under strings (or lists, if you will) and thatrev
is a sort of negation operation here. So if we view these as logical relations, then we get... something very similar to DeMorgan, anyway. ↩ 
The term "proof engineer" is used according to what I understand the guys at Data61 understand of it. They were hiring proof engineers last time I looked. ↩

This can be proven separately using the same techniques employed in the rest of the essay. Proving computational complexity represents in fact the first attempt at structural induction of most computer science students. ↩

Most programmers write a wrapper around that, but I've avoided doing this for the sake of a brevity... which is lacking anyway. ↩

The concept of fold, or catamorphism, from category theory provides some insight into this. No, we're not going to introduce another concept here, although the curious proof engineer is encouraged to look it up. ↩

Quantification is yet another important aspect in formal logic. Say, when you have something like
f(x) = x
, then this is in fact analogous to saying "given an arbitraryx
, thenf(x)
returnsx
". I've overlooked this in my initial list of assumptions, but in this particular case it makes a huge difference, kinda like the joke with uncle Jack off a horse. ↩ 
It took me about two hours, but I've been through this a while ago while playing with Benjamin Pierce's Software Foundations and Coq. ↩

Where "to scale" is used here in the "derived from prime mover" sense, i.e.:
mircea_popescu: davout something (convenience, anything else) is correct if it scales, which is to say is derived from the prime mover. anything else  incorrect.
mircea_popescu: sinful is also a proper attribute of incorrectness, because it is literally a headless spawn of the very devil.
davout: not sure i really get what you mean by "it scales"
davout: if you bundle lots of shit, it quickly becomes unmanageable
davout: because all abstractions and conveniences have a cost
mircea_popescu: not so. i can go from everything i do in an infinite string of correct whys to prime logic. broken shit can't do that.
davout: what's "prime mover" in this context?
mircea_popescu: possibly your idea of "scales" is tainted by the idiots, "to scale means to be used by a larger cattle headcount". that has nothing to do. to scale means to go up the abstraction tree. an apple is a correct apple if it scales, ie, if the concept of apple follows from it.
mircea_popescu: literally the aristotelian imperative. the first thing to have moved.[...]
mircea_popescu: all you need is a false implication somewhere, davout ; ANYWHERE. once you have it then everything becomes provable.

Formal verification was a thing for hardware way before the huge software systems that we have today emerged. It makes a lot of sense to verify hardware, as hardware is relatively simple to specify  at least in theory, if you don't count dinosaurs such as Intel's x86  and it absolutely has to work before it reaches the customer's shelf. This also holds true for some software, but even with a bare metal environment and a C compiler one can very easily run into unknown unknowns, which may cause the world to explode. ↩

See McCarthy, John. LISP 1.5 programmer's manual. MIT press, 1965. Particularly Chapter 1.6 (pp. 1014) describing the basic evaluation mechanism, and Appendix B (pp. 7072) describing
prog
, which can be used to implement iterative loops, particularly thedo
macro used by us here. ↩ 
I'm not venturing to guess what these terms mean today. In my particular variety of the English language it means "someone who knows reasonably well what they're doing with computers". ↩
In other lulz from the academic space, Australia's science agency pulls the plug on seL4: news piece; Heiser's comment.
From my obtuse angle, it looks like Australians have finally figured out that there's no strategic edge to this braindamaged approach of adding piles of machineedible annotations that no one else will read. Dude, specifications are meant to be consumed first by humans and then, maybe, as an afterthought, verified by machines. There's absolutely no point in rewriting the program as a spec in yet another broken programming language: it's expensive as hell and, owing mainly to the intrinsic property of computers of being systematically misusable, it yields very rarely and very little.
So in response, instead of addressing this first, you're embarrassing yourself by putting the matter yet again! on the todo list. What can I say, watching how this obtuseness will destroy you in the notevenallthatlong term will be sorta fun to watch... as fun as anything can be in the postcovid times.
While this was an interesting read, I can't claim to have read it as carefully as a mathematical topic deserves. Were some trap hidden therein, I didn't come across it.
I've decided upon a different method of proving software correct, one which doesn't require nearly so much thought. I for now call it Tabular Programming; this article applies it to Roman numerals:
http://verisimilitudes.net/20220131
The basic idea is that a great many things can be represented as a table access, but not everything; by using very simple composition rules, we can use such tables to represent infinity, however; thus the amount of code and computation is reduced to its bare minimum, and a hacker need only check the tables and the few, small rules to prove correctness. Such programs can trivially be made to have constant time and constant memory properties. Proving correctness can also be done mechanically, by simply comparing tables for equality, sparing the hacker thought for better things, and this mechanism is easilyunderstood.
For append and reversal, these methods are overkill; it clearly suffices to prove proper operation for empty list arguments, and then arbitrary lists, and a specialized calculus would make this much more concise. I've also read the LISP 1.5 programmer's manual, and don't recall McCarthy needing such things therein; the truth was obvious, the truths were the definitions.
Program correctness will come from correctly composing correct components, and I question how much intelligence truly be needed for this. I'll cease writing before I drone on further.
Perhaps you will find my proof of correctness for FFA Chapter 5 to be more interesting, but in essence it's another application of structural induction over a very specific programming problem, as is the one above. The difference is that the approach in the current article attempts to overformalize the mathematical proof for mechanical processing, which is unfortunately the curse of most (all?) "computerassisted proof systems" devised to date.
I like how that proof didn't focus on proving the constant time properties, and instead introduced explicit control to make it easier to prove. I should wait to comment on it until after I resume reading FFA.
So, no thoughts on my method, then?
Consider a more interesting way to prove those two list algorithms: Consider using a very small memory space of linkedlists, so that every possibility may be enumerated; prove every possible combination be correct; prove the algorithm doesn't depend on the memory space, which can be done by construction; and then prove the size of the memory space be irrelevant. This can be done mechanically, to good success. Machines can easily compare billions of values; they should be used like this to prove things more often.
In re: tabular programming: it reminds me on one hand of the socalled "propertybased testing", which may be used to automatically generate (as in your linkedlist example above) tests emerging from a prespecified general property, which can be then mechanically verified. On the other hand: are you familiar with cellular automata? The tables remind me of that.
I suppose there are worse names than propertybased proving, and it fits well enough. I'll still call it by the name I've already chosen.
Yes. Well, the most general such implementations are simple table indexing, so I can certainly see the relation.
It's very freeing, to be able to prove a program works, without thinking about it.
[...] When trust as a whole is broken or otherwise disappears by some other means, society collapses and war ensues. That is not to say that lack of trust (or distrust) is necessarily a cause of war; after all it is not that Genghis Khan didn't trust the peoples he conquered, but that he conquered them first and foremost because he could. Lack of trust is also not a problem in and of itself  (too much) trust is, especially when it is not accompanied by verification. [...]
[...] first part of this journey consisted in studying software that is formally verified at huge costs and which doesn't really fit in head. Fortunately I was also working on some practical problems at [...]