Re: [Gnu-arch-users] Managing changes to projects that use autoconf/automake with tla

[Robin Green]

On Tue, Apr 06, 2004 at 08:49:03AM -0700, Tom Lord wrote:
> What if the problem were solved tomorrow -- if we could, as you put
> it, stick some wings on that fish?
> 
> One can only speculate.  I speculate that alternative kernels and libc
> implementations would be more viable, that the form and function of
> the platform distribution business would shift away from
> consolidation, that test-based certification would be more important,
> that packages would be significantly less interdependent, and on and
> on.

Here is my perspective:

1. Integration bugs are always bugs, not "user errors", contrary to some
hotheads in the GNU/Linux community. If a dependency specification is
missing or inaccurate for package P, this is a bug _in_ package P. If
a tarball doesn't contain any dependency specifications, it is probably
replete with such bugs :)

2. Test-based certification is nice, and a useful stopgap, but proof-based
certification with formal methods provides a better quality guarantee
of correct operation.

Obviously, proof-based certification is a large project. :)
I intend to attack the problem with:
(a) a new programming language system with a proof verification system
built-in, and eventually
(b) a user-mode operating system (like User Mode Linux, but not Linux!) with
full proof traceability down to at least the host OS.

(Last time I mentioned this, Tom told me to go back to the 1960s or something
;-)
-- 
Robin

pgpiZoLLjfDyT.pgp
Description: PGP signature