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 <
barak@pearlmutter.net> wrote:
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.