Re: Extending discriminant types

[Ludovic Brenta <ludovic@ludovic-brenta.org>]

On Nov 26, 4:49 pm, Adam Beneschan <a...@irvine.com> wrote:
> 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.

I'd second that. In order not to overburden anon, I'd not require him
to report on his progress until he's finished.

--
Ludovic Brenta.
Eternity is long, especially towards the end.