Interfacing with normal Rust code

[bvssvni]

willi_kappler asked whether it is possible to one day implement dependent types or refinement types in Rust as a crate.

There might be several ways to do this.

For example, one idea is to use TypeId and a hash table to look up function pointers.

Another approach could be to use Prop types together with normal Rust code.

Yet another idea is to use a solver that generates proofs in Rust.