What is the purpose of the 3 different codebases?

[ProofOfKeags]

There are three main segments to this repository:

1. C
2. Haskell
3. Coq

My rough understanding of the roles each of these play are that the C code is intended to be the execution environment that would be deployed to consensus. This is the interpreter people will be running in node implementations. The Haskell code is primarily the means by which we generate simplicity expressions. The Coq code is there to prove theorems about individual simplicity expressions so that we can leverage simplicity's nice theoretical properties to gain more higher level assertions that we would want out of contracts deployed in simplicity.

Is this a correct assessment? If not, where is it wrong?

This discussion was inspired by some off-topic discussion in #83

[roconnor-blockstream]

There is also

4. Rust

My view is that the C code is for consensus purposes. The Haskell code is a reference implementation. The Rust code would be for creating Simplicity Programs. The Coq code will be for proving things about Simplicity programs, and in combination with VST, proving the correctness of the C jets and maybe even the whole C implementation of the Simplicity interpreter.

[dr-orlovsky]

How to make sure these four codebases are equivalent, and, for instance, that the statements about simplicity program proven with Coq will apply for rust-written program?

[roconnor-blockstream]

All the code bases have independent implementations of functions to compute the Merkle root of Simplicity expressions. So if the Merkle root of a Simplicity expression matches between the Rust and Coq implementations, we have reasonably high assurance that those expressions are syntactically identical. Errors in the implementation of the Merkle root will more likely just cause unexpected mismatches of identical expressions rather than accidentally causing two different expressions to end up with the same Merkle root (due to one of the implementations being wrong).

I currently rely on some amount of randomized testing to assure that the C implementation matches the Haskell implementation (via FFI bindings of the C implementation to Haskell). Longer term I'd like to use VST to prove that the C implementation matches the Coq implementation.

The Coq and Haskell implementations are similar enough that I'm confident that their implementations are the same. The Core Simplicity language is simple enough, that in a strongly typed language, such as Haskell and Coq, it is very hard to make an implementation error. We will need to be more careful about the implementation of primitives (not yet available in Coq) and should try to make the code between Haskell and Coq as similar as possible.

[dr-orlovsky]

Alright, I misunderstood originally. These implementations are implementations of the simplicity, not jets. It is the problem with jets implementation which should be proven to be equivalent to the simplicity expression.

[ProofOfKeags]

The Coq code will be for proving things about Simplicity programs, and in combination with VST, proving the correctness of the C jets and maybe even the whole C implementation of the Simplicity interpreter.

This is how that equivalence proof would be accomplished.