Neta

* Compilation correctness
* How to write secure smart contract in Coq and extract it to SCaml/LIGO or whatever.
* 5-7

* ~~Liquidity~~
* LIGO (PascaLIGO **CameLIGO** ReasonLIGO)
* SmartPy (Python library)

CameLIGO
* no pattern match
* bugs
* not strictly ocaml

SCaml
* TypedAST => Michelson
* Cheap
* OCaml compatible

[Juvix](https://github.com/cryptiumlabs/juvix)

# SCaml project ideas

## Write examples!

### Contract a day in SCaml

[Contract a day series](https://www.michelson-lang.com/contract-a-day.html) is *obsolete* but contains lots of smart contracts in Michelson. Note that it uses *very old* Michelson which has *return types*. Though old, it is still interesting series. Let's have the equivalent one in SCaml and publish small blog series.

Current status
: 50% of contracts are already translated into SCaml.

### Implement TZIPs

[TZIP](https://gitlab.com/tzip/tzip) (TeZos Interoperability Proposals) defines interfaces for dApps and smart contracts. Implement some of them and see whether SCaml is enough powerful for them.

Current status
: SCaml can easily implement FA1 (TZIP-5), but we found it hard to test.

## Certified compilation

The compilation algorithms from the subset of OCaml to SCaml's intermediate language, then to Michelson are pretty straightforward. I think they are feasible to prove the correctness: the semantics of OCaml, IML are preserved by the compilation to Michelson.

* In Coq? The compiler must be all rewritten in Coq.
* In F\*? We can gradually port OCaml modules to F\*. Cons: not so many experts we have.

### Mini OCaml

A subset of OCaml with pattern match and user defined types. Currently the implementation has no language layer for it. Translation from OCaml to Mini OCaml is trivial and ts correctness is assumed.

### Certificaition of compilation to IML

Mini OCaml - pattern matching - user defined types.

* Type encoding of user defined types into binary tuples and sums
* Pattern match compilation

### Certificaiton of compiliation to Michelson

Can we use Mi-Cho-Coq ?

## "Certracts", certified contracts

By Coq/F\*, extracted to SCaml.

Assuming the compilation correctness of OCaml and SCaml and the correctness of SCaml compilation to Michelson, we can write contracts whose specifications are proven in Coq or F\*.

### Coq to SCaml

* What sort of properties we want to prove?
* SCaml does not have modules nor polymorphism. Is it easy to extract to such a limited language?

## dApps in 1 language

OCaml can be used for all the layers of dApp development:

* Smart contracts in SCaml, compiled to Michelson
* Server side in OCaml, compiled to native code
* Web UI in OCaml, compiled to JavaScript

These layers can share the same code, which makes dApps development normally done in polyglot much much easier.

## New language features

* Labeled arguments
* Record in variants
* Polymorphism
* Separate modules
* Code optimization
* Contract origination/invocation mechanism in SCaml

## Simulation in OCaml

Simulation of SCaml primitives.

## Contract test environment

OCaml programable interface to:

* Deploy
* Call
* Investigate storage

of SCaml/other contracts.