You could consider the compiler for the IO type part of the TCB and execute
source code with caching, like nix. Every process could be wrapped in an IO
sandbox that is enforcing the types for all IO operations.
That just requires being able to implement a->Maybe b i.e. have a fixed
binary representation for the data in and out of the inner program.
Something like rudimentary programmable scripts that run on kernel system
call invocations already exists in Linux, so it could be possible to
compile down to that.
Alexander
2018, 17:04 Barak A. Pearlmutter
At a high level, you seem to be proposing encoding and enforcing safety properties of executables using a type system. One instantiation of this idea is proof-carrying-code (Necula and Lee, 1996, see https://en.wikipedia.org/wiki/Proof-carrying_code), which ensures safety properties of machine code. The spin-off Cedilla Systems built a mobile OS (intended for phones) around this, with the idea that third-party apps would run unprotected with safety guaranteed solely by sophisticated use of types. The Fox Project, http://www.cs.cmu.edu/~fox/, was philosophically similar, and their web page contains a bunch of interesting pointers to relevant work.
For whatever reason, this stuff never got much penetration. But in today's Internet of Things, with malware being injected into mobile phones and cars and light bulbs and toothbrushes and smart dust, it may deserve another look. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.