<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>The problem with an IR is that some languages would inevitably
suffer - LLVM in particular was designed as a backend for a C
compiler, and so it is not necessarily well-suited for lazy
languages, immutable languages, etc. (not to mention
self-modifying assembly and other such pathological beasts...)<br>
</p>
<br>
<div class="moz-cite-prefix">On 10/06/2018 08:31 PM, William Yager
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAG8oi1Odghy4FfdACtKsGVUnJ1XZEd3rzBGEsTG-hiLj7V5BbQ@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<div dir="ltr"><br>
<br>
<div class="gmail_quote">
<div dir="ltr">On Sat, Oct 6, 2018 at 11:03 PM Barak A.
Pearlmutter <<a href="mailto:barak@pearlmutter.net"
moz-do-not-send="true">barak@pearlmutter.net</a>>
wrote:<br>
</div>
<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" moz-do-not-send="true">https://en.wikipedia.org/wiki/Proof-carrying_code</a>),
which<br>
ensures safety properties of machine code. </blockquote>
<div><br>
</div>
<div>I would guess a factor that prevented something like PCC
from taking off is the fact that proofs over binaries are
relatively pretty challenging to express and verify, and ISA
semantics tend to be really complicated.</div>
<div><br>
</div>
<div>I think an intermediate approach that might be a lot
cheaper to implement is to ship some sort of IR (rather than
machine code) that is A) relatively cheap to check and
compile and B) carries some variety of safety guarantee.</div>
<div><br>
</div>
<div>As I recall, A) is already in use. Apple requires
developers to submit applications as LLVM IR rather than
machine code.</div>
<div><br>
</div>
<div>LLVM IR definitely isn't designed with B) in mind,
however. I could imagine something like Core being useful
here. A fully annotated type-checked language with semantics
amenable to formal analysis.</div>
<div><br>
</div>
<div>You could add some sort of effects system to the type
system of the IR, as a basis for enforcing security
policies. E.g. network access could be an effect.</div>
<div><br>
</div>
<div>The advantage of doing this over PCC is that we don't
have to retrofit the proof system to match the ISA, but
instead can design the IR specifically to make the proof
system easy. A downside is that you have to compile the
application once upon downloading it, but this doesn't seem
to cause too much of an issue in practice.</div>
<div><br>
</div>
<div><br>
</div>
<div> </div>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a>
Only members subscribed via the mailman list are allowed to post.</pre>
</blockquote>
</body>
</html>