Xavier Denis

Another issue I've found: the `ghost!` macro does not work well when storing ghost values in types, it doesn't compile properly when compiling in passthrough mode (not creusot).

> We need to take care about portability of the proofs, though. That's the tricky thing, especially in the presence of generics, what is `SizeOf([T; 2])`? > E.g., what do...

The idea I have here is that once we have cloneable types in Creusot, a type module defines the type, but also the `size_of` and `align_of` of the type, potentially...

> If we need Ghost resources, then we could use ghost resource types such as Seq or synthetic tokens, as part of the non-ghost code. Functions of the Seq module...

I still think that there are three levels at play, already: program code, linear ghost code, and pearlite (non-linear ghost code), why not just make those equally accessible in programs?

> So these resources are just another kind of resources the we want the borrow checker to take into account, in addition to plain physical resources. Yes but it feels...

> How is this different for Ghost? When you pass a Ghost parameter, it is seen by rustc as a zero-size value. I don't know whether there are situations where...

heterogeneous or homogeneous? I feel like homogenous would be nice but at the same time, I would like to be able to add a `u64` to an `Int`.

True, but we need to make sure to leave holes for special traits like `Add`, `Index` etc

Even then, we will need to special case `Deref` at the very least, but yes.