<div dir="ltr">Heh, ok, segfaults themselves are a red herring.  More precisely:<div><div><br></div><div>The operational semantics for a SafeIO language should always accurately model its memory state.  The application should not compute (take a step in the semantics) in a way that exposes corrupt memory or arbitrary undefined behavior.  Nor should it violate the memory model.</div><div><br></div><div>Moving immediately to the "Terminated" state is fine, whether it be due to out-of-memory, kill -SEGV, cosmic rays, or hardware failure.  An FFI call that corrupts memory is bad (may result in arbitrary behavior, not just termination) as is ptrace'ing.</div><div><br></div><div>Naturally, all Unsafe code is part of the TCB, as is the OS and GHC, and low-level data structure libs and bindings.  It's a big TCB.  Still, it's something to be able to write an app that doesn't automatically get added to this TCB just by virtue of being an <i>app</i> (main::IO).</div></div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Aug 9, 2016 at 10:52 PM, Brandon Allbery <span dir="ltr"><<a href="mailto:allbery.b@gmail.com" target="_blank">allbery.b@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><span class=""><div class="gmail_quote">On Tue, Aug 9, 2016 at 4:19 PM, Edward Z. Yang <span dir="ltr"><<a href="mailto:ezyang@mit.edu" target="_blank">ezyang@mit.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>If you can execute subprocesses, you could always spawn gdb to<br>
attach via ptrace() to the parent process and then poke around<br>
memory.</div></blockquote></div><br></span>Don't even need that if you're just talking segfaults, you can always spawn a subprocess "kill -SEGV $PPID" :)</div><div class="gmail_extra"><br></div><div class="gmail_extra">Unless you have full control over all the code that could be run in subprocesses, it's not going to be safe much less Safe.<span class=""><br><div><br></div>-- <br><div data-smartmail="gmail_signature"><div dir="ltr"><div>brandon s allbery kf8nh                               sine nomine associates</div><div><a href="mailto:allbery.b@gmail.com" target="_blank">allbery.b@gmail.com</a>                                  <a href="mailto:ballbery@sinenomine.net" target="_blank">ballbery@sinenomine.net</a></div><div>unix, openafs, kerberos, infrastructure, xmonad        <a href="http://sinenomine.net" target="_blank">http://sinenomine.net</a></div></div></div>
</span></div></div>
</blockquote></div><br></div>