The Coq mailing list

[Faré <fahree AT gmail.com>]

Dear Coq club,

our startup, Legicash, is looking for a Coq programmer and/or academic
collaborators to develop "smart contracts" on cryptocurrency ledgers
(first intended target: Tezos).

Our approach, as distinguished from others (e.g. Plasma.io), views
contracts not as arbitrary code to run, but as referees for
interactive proofs that verify propositions using Game Semantics (see
details below if interested).

We are looking for a full time prover / programmer but also for
part-time collaborators, and/or a long term collaboration between
industry (our startup) and research (your lab). We are confident that
we will get funded real soon now (within a few weeks).

Experience with embedding a DSL in Coq, extracting code from
specifications, Game Semantcs, Computability Logic, Ludics, Linear
Logic, Epistemic Logic, Cryptocurrency ledgers, network protocols,
consensus protocols, transactional databases, etc., are pluses.

We are based in Boston and NYC. You don't have to be, but it's also a
plus if you are or can be.


More details, for those interested:
* Smart contracts are made of clauses of the form "This party promises
that this proposition holds, or else will be sanctioned".
* Sanctions are of the form "this party immediately pays that party
this amount, and that record is published".
* Predicates have quantifiers over the contents of one or several
blockchains or similar data structures — finite (though potentially
large) data structures known by all participants.
* To ensure data structures are indeed known by all participants, a
separate/new/amended blockchain is provided as a "court registry" that
creates shared knowledge, while the usual smart contract blockchain is
a "judge" that builds the slower and more expensive common knowledge.
* A verification game consists in one party providing witnesses for
the topmost existential quantifiers, and when reaching universal
quantifiers, challenging the other party to provide a witness for the
negation of the proposition.
* All participants post bonds sufficient to guarantee payment if they
are found wrong.
* Clauses are always guarded by a proposition that detects that the
case was never resolved or settled before.
* The surface logic has elements of linear logic (tokens, claims,
etc., can't be duplicated) that are translated into propositions about
appropriate witnesses.
* For security against failing victims or collusion between
participants, games actually can involve third parties that complete
arguments made with suboptimal strategies.
* With all the above infrastructure, develop suitable economic
protocols, for e.g. fast payments, safe cross-chain swaps, insurance,
etc.

Code extraction:
From a single specification in Coq, we will extract:
1- proof of correctness properties (accounts are well-balanced,
account holders can get their money back, etc.).
2- code (in OCaml?) that manipulates the data structures involved
(typically "side-chains") and handles the network protocol.
3- the contract that embodies the referee in the corresponding
verification games.
4- the optimal legal argument strategies for each participant to play
these verification games.
5- end-to-end integration test cases to check that the complete system
can indeed handle all difficult situations in practice.


This is an ambitious project that aims to change how "smart contracts"
are written by making formal methods an essential tool.

Please respond privately; do not Cc: the list unless you have remarks
to share with everyone.

—♯ƒ • François-René ÐVB Rideau •Reflection&Cybernethics• http://fare.tunes.org
Patterns mean "I have run out of language." — Rich Hickey