On 24/09/17 18:06, Emanuel Berg wrote:
> Hold - perhaps the verification has to be
> verified as well?

What any proof of correctness proves is an implication saying roughly:
“IF the environment meets these requisites THEN the program does […]”.

The “bugs” described in the aforementioned paper are not a flaw in the
proof. The source of the problem is that EITHER the programs under test
were being used in an environment does not meet the requisites (i.e.:
“IF the environment meets”) OR the user was expecting the program to do
something different than what is guaranteed by the conclusion “the
program does […]”.

> C'mon now, this is just another
> Computer Science hangup. Just like
> functional programming, or testing for that
> matter - which also is an academic pursuit, by
> the way! [1] - but as always, there is no
> silver bullet solution.

This is the prevalent attitude among programmers, and this is the reason
that we are showered by an endless stream of security patches and bug fixes.

> If I'd send the space fleet to the oldest
> galaxies of the universe, I'd like all methods
> anyone could think of to make as sure as
> possible the software is correct.
> 
> I'd start with very skilled and motivated
> programmers, proceed with sound programming
> practices, then code review, and then
> excessive testing.
> 
> I suppose formal verification would be
> a distant fourth.

Well, then it is a very good thing that you are NOT in charge of
designing that piece of software.

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