On 24/09/17 01:47, Emanuel Berg wrote:
> A very, very small fraction of programmers will
> ever care to (or indeed be able to) create
> a model of the program just to verify the model
> and then verify that the model is in agreement
> with the program - this is just insane to ask
> of anyone, and it isn't realistic one bit to
> ever be a practical alternative.

That is not how formal verification works in practice. Instead many
(probably most) tools work by programming directly in the logic of the
proof assistant and then extracting (without manual intervention) a
program in a conventional programming language that has the same
behavior as what was programmed in the logic.

Contrary to what you assert, there are computer program well beyond
trivial that have a specification and proof of correctness. I already
mentioned the CakeML compiler <https://cakeml.org/>. Other examples are
the seL4 microkernel <https://sel4.systems/> and the Compcert compiler.

It is true that formal verification of a program requires several times
the effort compared to writing a comparable non-verified program (but
with many bugs). I argue that this effort is necessary, because it is
the only way to write correct software.

I think you will agree that although writing undocumented software is
easier than writing well-documented software, writing documentation is
part of software development and thus undocumented software must be
considered incomplete. In the same way, I extend this to the claim that
formal verification is part of software development and thus unverified
software is incomplete.

Although writing incomplete software is easier than writing complete
software, the task should not be considered solved. It is like just
building half of a bridge. Surely it is easier than building all of it;
but it is not enough.

> To a compiler - ? This can be done with simple
> shell tools that perform basic computation!

If by “simple shell tools that perform basic computation” you mean
testing with random inputs, note that I already explained why this will
be an awful testing method for a compiler. I will not repeat the
explanation.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan