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.<div><br></div><div>  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.</div><div><br></div><div>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.</div><div><br></div><div>Alexander</div><div><br></div><div> 2018, 17:04 Barak A. Pearlmutter <<a href="mailto:barak@pearlmutter.net">barak@pearlmutter.net</a>> wrote:<div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">At a high level, you seem to be proposing encoding and enforcing<br>
safety properties of executables using a type system. One<br>
instantiation of this idea is proof-carrying-code (Necula and Lee,<br>
1996, see <a href="https://en.wikipedia.org/wiki/Proof-carrying_code" rel="noreferrer" target="_blank">https://en.wikipedia.org/wiki/Proof-carrying_code</a>), which<br>
ensures safety properties of machine code. The spin-off Cedilla<br>
Systems built a mobile OS (intended for phones) around this, with the<br>
idea that third-party apps would run unprotected with safety<br>
guaranteed solely by sophisticated use of types. The Fox Project,<br>
<a href="http://www.cs.cmu.edu/~fox/" rel="noreferrer" target="_blank">http://www.cs.cmu.edu/~fox/</a>, was philosophically similar, and their<br>
web page contains a bunch of interesting pointers to relevant work.<br>
<br>
For whatever reason, this stuff never got much penetration. But in<br>
today's Internet of Things, with malware being injected into mobile<br>
phones and cars and light bulbs and toothbrushes and smart dust, it<br>
may deserve another look.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div></div>