On 22/09/17 17:14, Emanuel Berg wrote:
> Also, formal verification that is applied on
> a model will only prove that *the model* is
> correct, not the real thing.

You seem to be confused, verifying that a program is correct *requires*
a model. Verifying the model is a different and separate task.

> […] Then it is trivial to setup a test
> program that will just invoke repeatedly with
> randomized integers and strings. […]

Random testing is very inefficient because most inputs are garbage and
are treated uniformly by the program under test. For example, feeding
random input to a compiler will result almost surely in only ill-formed
programs and thus will not exercise anything but the parser. Good
testing must exercise code paths that only run in rare corner cases and
the probability that random testing achieves this is very small.

But like I said, testing is fundamentally flawed. Testing can tell you
that a program is defective, but not that a program is free from defects!

> There are also languages like Dafny where you
> can state formally what a function should do,
> and the verification tool will match that to
> your code. […]

Taking a glance at Danfy, it seems like it trusts the answers of a SMT
solver (Microsoft's Z3) and does not generate proofs of correctness (but
I can easily be wrong; I did not check in deep because I dislike .NET).
This is not what I am referring about when I say “proving programs
correct”. I mean software like CakeML <https://cakeml.org/>. It is
linked to a proof assistant (HOL4). You can develop there the
specification of the program and prove it correct according to the
specification.

There is still much work to be done to make formal verification tools
like this more usable, but it must be noted that in the case of CakeML
it *already* works. CakeML is itself formally verified using HOL4.

Unfortunately there is little documentation material to learn to use
CakeML. Using HOL4 or other proof assistant requires at least a solid
intuition for formal logic and some knowledge in mathematics. Anybody
wanting to call himself a programmer must become comfortable with using
a proof assistant because this is a prerequisite to writing correct
software. *ANY* other approach leads to defective software, *especially*
ordinary testing[1].

Notes:

[1]: There is also software that is not itself proved correct, but
generates a solution for a problem along with a proof that the solution
is correct. For example, many SAT solvers meet this description.
Provided one can verify the proof, one can the ascertain that the
solution is correct, but the program may still generate incorrect
“solutions” in other cases.

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