Re: Extending discriminant types

[Adam Beneschan <adam@irvine.com>]

On Nov 26, 3:05 am, Ludovic Brenta <ludo...@ludovic-brenta.org> wrote:

> anon's theorem: the number of bugs in a program decreases with time
> and eventually reaches zero, whether or not anyone maintains the
> program. (However, to observe this theorem, someone must use the
> program.)
>
> I'd be interested in anon's proof of that theorem. That would
> definitely make it into the Jargon file :)

I'm not sure that it could be proven mathematically, but perhaps it
could be tested.  In particular, we could test whether this theory or
the contrary theory is true, the contrary theory being one that you
posted earlier in this thread:

## Even an infinite amount of testing cannot prove a program to be
bug-
## free; it can only uncover an infinite amount of bugs.

While this may not be literally true---I suspect it is mathematically
impossible for a finite compiler to have an infinite number of bugs---
it could be reformulated in a way that makes it amenable to testing.
My proposal, then, is that if anon can't prove his theory formally, we
should ask him to do it empirically by performing an infinite amount
of testing on GNAT, and then coming back to comp.lang.ada and
reporting on the results once this testing process is complete.

                                -- Adam