Re:The Synthesis Kernel (1988) [pdf]
by kazinator on Tuesday August 22, 2017 @09:54PM
(#15077930)
It would have to be formally verified, because there is no informal way to have any confidence in this sort of thing.
The informal way is to have a team pore over code. Here, the body of code is some unbounded, dynamically generated set of little routines that are individually correct with respect to an unfolding run-time situation (not in and of themselves). Good luck, know what I mean?
If you log all the generated pieces of code, you don't know whether you have the whole set of them that can be. If not, there could be the bugs in the ones you don't have. Then there is the monstrous task of going through them, and somehow correlating each one to the situation that was unfolding (maybe with the help of additional logged information).
A static, monolithic piece of code can be checked from alpha to omega; you know what you have looked and haven't looked at, and when you're done. Sure, it has the usual combinatorial explosion of possible code paths making the task hard, but compared to a whole dimension of synthesized code, it looks like a walk in the park.
If you want to use currying to speed up operating system calls, get rid of the kernel/user boundary and have the whole system (application(s) plus kernel) in a functional language and have them running in one image. Then you can use actual currying (or closures, continuations). Those techniques don't require dynamic code synthesis.
The informal way is to have a team pore over code. Here, the body of code is some unbounded, dynamically generated set of little routines that are individually correct with respect to an unfolding run-time situation (not in and of themselves). Good luck, know what I mean?
If you log all the generated pieces of code, you don't know whether you have the whole set of them that can be. If not, there could be the bugs in the ones you don't have. Then there is the monstrous task of going through them, and somehow correlating each one to the situation that was unfolding (maybe with the help of additional logged information).
A static, monolithic piece of code can be checked from alpha to omega; you know what you have looked and haven't looked at, and when you're done. Sure, it has the usual combinatorial explosion of possible code paths making the task hard, but compared to a whole dimension of synthesized code, it looks like a walk in the park.
If you want to use currying to speed up operating system calls, get rid of the kernel/user boundary and have the whole system (application(s) plus kernel) in a functional language and have them running in one image. Then you can use actual currying (or closures, continuations). Those techniques don't require dynamic code synthesis.