The userbase for 2.1.x kernels is a lot of it
> Are preconditions and postconditions enablable where they make sense?
No, and for many things it would be hard. There is probably an interesting
project in there somewhere
> Could we do mathematical proofs of algorithms used in Linux, especially
> the really critical ones?
Almost all the core small algorithms in Linux are 'obviously correct'
which means they normally work right 8). Proving bigger stuff is hard
nobody Ive seen has yet really managed to mathemtically describe such
complex interactions, and before that you'd need to prove the compiler
and the CPU and its microcode
Building an optional compiled in set of constraints for entry/exit is
doable, I think the rest becomes rapidly infeasible
Alan
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu