X-List-Received-Date: Tue, 07 Jun 2022 04:12:10 -0000
--000000000000afa64e05e0d3ca52
Content-Type: text/plain; charset="UTF-8"
An interesting idea is what I'd call "proof specificity".
The motivation is to prove that certain classes of bugs
cannot occur. Or, more generally, that certain classes of
behavior cannot occur.
At a very low level there could be a proof that the stack
size is bounded.
A slightly higher level might prove that the implements a
proper protocol such as an FTP copy operation.
Next up might be proving optimizations are correct, for example,
a peephole optimization of register operations. The optimizations
applied during intermediate representations such as loop unrolling
are also interesting.
At the numeric algebra level there are proofs that over/underflow
cannot occur, nor can there be a divide by zero.
At the symbolic level there can be proofs of things like matrix
operations at the algorithm and specification level, independent
of the implementation.
Of course, the holy grail involves proofs that the implementation
implements the specification correctly.
Designing an architecture to support such proof specificity is a
challenge.
Tim
--000000000000afa64e05e0d3ca52
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
An interesting idea is what I'd call "proof =
specificity".

The motivation is to prove that=
certain classes of bugs

cannot occur. Or, more generally, that c=
ertain classes of

behavior cannot occur.

At a very low level there could be a proof that the stack

size i=
s bounded.

A slightly higher level might prove tha=
t the implements a

proper protocol such as an FTP copy operation.=

Next up might be proving optimizations are correc=
t, for example,

a peephole optimization of register operation=
s. The optimizations

applied during intermediate representations =
such as loop unrolling

are also interesting.

=
At the numeric algebra level there are proofs that over/underflow

cannot occur, nor can there be a divide by zero.

=

At the symbolic level there can be proofs of things like matrix

<=
div>operations at the algorithm and specification level, independent

<=
div>of the implementation.

Of course, the holy gra=
il involves proofs that the implementation

implements the specifi=
cation correctly.

Designing an architecture to sup=
port such proof specificity is a

challenge.

<=
div>Tim

--000000000000afa64e05e0d3ca52--