[Simplicity] Questions about Simplicity

[Russell O'Connor]

Hi Chris,

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.

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.

Regarding the Adga issue, I responded in another thread
<https://lists.ozlabs.org/pipermail/simplicity/2018/000011.html>.

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.

There are several other fronts of work that could be done with Simplicity
simultaneously.

* 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.
* We need a formally prove the correctness of the real libsecp256k1 C
library using VerifiableC <http://vst.cs.princeton.edu/>, but that requires
a license to use 'clightgen'.
* We also need to formally connect this libsecp256k1 specification to
crypto math, for example, by formally connecting it to the fiat-crypto
<https://github.com/mit-plv/fiat-crypto> library or some other similar Coq
library.
* Related, is that the fiat-crypto <https://github.com/mit-plv/fiat-crypto>
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.
* 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.
* 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.
* 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.

On Fri, Dec 21, 2018 at 11:47 AM Chris Stewart <chris at suredbits.com> wrote:

> Hi Simplicity Mailing list,
>
> 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
>
> 1. How "final" is Simplicity's language design? Is there still unanswered
> questions?
> 2. Is the Coq code up to date with Simplicity's haskell implementation?
> 3. Is the Agda library published any where?
> 4. What projects would be good for a grad student to work on related to
> Simplicity?
> 5. What are the current hurdles (excluding political) that keep Simplicity
> from being adopted
>
>
> In short, what is the best way researchers can help out, and what is the
> best way average developers can help out.
>
> -Chris
> --
> Simplicity mailing list
> Simplicity at lists.ozlabs.org
> https://lists.ozlabs.org/listinfo/simplicity
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ozlabs.org/pipermail/simplicity/attachments/20181224/395bb427/attachment.html>