<div dir="ltr"><div class="gmail_quote"><div>Hi Chris,</div><div><br></div><div>So I reserve the right to make adjustments to the Simplicity language if issues arise. However, I don't really expect any changes to the language, especially with respect to the Core language combinators. I suppose it is possible the exact details of the 'disconnect' combinator could change as there is a small area of design space around there and, while I think I have picked a good one, I don't really have any practical experience using it yet. Details about how type inference precisely works with respect to sharing and specific details about serialization format will probably see minor amendments.<br></div><div><br></div><div>The Coq and Haskell implementation and the technical report should be in line with each other, and if they are not, it is an error. Some aspects maybe implemented in Haskell but not yet implemented in Coq. The denotational semantics should be implemented in everything.<br></div><div><br></div><div>Regarding the Adga issue, I responded in <a href="https://lists.ozlabs.org/pipermail/simplicity/2018/000011.html">another thread</a>.</div><div><br></div><div>I'm working towards making a branch of Elements that uses Simplicity. To this end, I'm currently working on a C interpreter for Simplicity.</div><div><br></div><div>There are several other fronts of work that could be done with Simplicity simultaneously.<br></div><div><br></div><div>* We need a formal specification (both low level and high level) of the libsecp256k1 implementation in Simplicity and a proof that the libsecp256k1 Simplicity implementation meets that specification.</div><div>* We need a formally prove the correctness of the real libsecp256k1 C library using <a href="http://vst.cs.princeton.edu/">VerifiableC</a>, but that requires a license to use 'clightgen'.<br></div><div>* We also need to formally connect this libsecp256k1 specification to crypto math, for example, by formally connecting it to the <a href="https://github.com/mit-plv/fiat-crypto">fiat-crypto</a> library or some other similar Coq library.</div><div>* Related, is that the <a href="https://github.com/mit-plv/fiat-crypto">fiat-crypto</a> library has implementations of crypto primitives for many different curves. These implemenations could be translated to Simplicity (with formal correctness) in order to make them all into Jets.</div><div>* I have an open problem that unfortunately isn't written up in detail yet, but essentially asks if Simplicity's type inference can use polymorphic type inference instead of monomorphic type inference without opening of Denial of Service attacks? Polymorphic type inference takes exponential time in the worse case (as opposed to monomorphic type inference which can be done in linear (or more realistically quasi-linear) time); however, polymorphic type inference also allows for exponentially smaller terms on some cases too. So if polymorphic type inference only takes exponentially more time in those cases where we use exponentially smaller terms, then there is no real cost to using it and many benefits that go beyond the exponentially smaller amounts of bandwidth used in some cases.</div><div>* Another PLish issue is that Simplicity is a low level language as we want a higher level language to create and optimize Simplicity expressions. Like something that uses variables names would be nice, and automatically stores the local environment in a balanced tree.</div><div>* Even better would be an even higher level language to specify entire protocols (e.g. the Lightning protocol) from which Simplicity expressions and other parts of the communication protocol could be formally derived and reasoned about.<br></div><div><br></div><div dir="ltr">On Fri, Dec 21, 2018 at 11:47 AM Chris Stewart <<a href="mailto:chris@suredbits.com">chris@suredbits.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Hi Simplicity Mailing list,</div><div><br></div><div>I was having coffee with a former professor of mine who is a PL researcher and talked to him about Simplicity. This lead to many questions I have about the state of the project</div><div><br></div><div>1. How "final" is Simplicity's language design? Is there still unanswered questions?</div><div>2. Is the Coq code up to date with Simplicity's haskell implementation?</div><div>3. Is the Agda library published any where?<br></div><div>4. What projects would be good for a grad student to work on related to Simplicity?</div><div>5. What are the current hurdles (excluding political) that keep Simplicity from being adopted</div><div><br></div><div><br></div><div>In short, what is the best way researchers can help out, and what is the best way average developers can help out. </div><div><br></div><div>-Chris<br></div></div>
-- <br>
Simplicity mailing list<br>
<a href="mailto:Simplicity@lists.ozlabs.org" target="_blank">Simplicity@lists.ozlabs.org</a><br>
<a href="https://lists.ozlabs.org/listinfo/simplicity" rel="noreferrer" target="_blank">https://lists.ozlabs.org/listinfo/simplicity</a><br>
</blockquote></div></div>