Hello everyone, This post is reviving the an old (RFC issue)[Add dependent types · Issue #2709 · rust-lang/rfcs · GitHub].
I scouted this forum and bunch of random places over the internet for progress on dependable types for rust and this is a discussion of my findings.
The goal of this post is to come up with a plan for RFC for adding dependable types to rust.
First why would we need dependable types. Dependable types is a very powerful tool, but for rust I can imagine two mainline use-cases 1- Proof carrying code in rust: this sounds a bit too specific but that may make rust lucrative for writing cryptographic primitives and code where the correctness (beyond basic memory safety) is important. 2- Type inference in procedural macros for free: I am not 100% sure that this use-case works. but intuitively I would think that since it is possible to pass types as arguments in dependable type system, this should somehow allow rust to model its own type system in runtime, and that may be used in procedural macros (That might as well be 100% wrong, I cannot fully imagine yet how would that work).
It would be possible to combine both use-cases DSL in rust that evaluate at compile time with stricter typing rules thus allow people to write rust code with more guarantees without having to deal with dependent types themselves.
** Which type system **
One of the main questions here is which type system to use, I am aware of 3 languages with dependable types, Coq, Agda and twelf. Both Coq and Agda are built on different views of Matrin Löf type theory, and twelf is built on Edinburgh Logical Framework. The advantage of having similar construct in rust is that the core type system would be extremely small, and provable to be correct which is a good thing. The disadvantage is that much of rust's features (pretty much everything) will have to be modeled on top of those extremely small type system, that would be extremely horrible in terms of performance since it is mostly functional programming model, besides that is counter productive since lots (if not most) of the stdlib would need rewriting(unless I am missing something).
The other extreme would incrementally add ideas from dependable types to rust. The problem is that we will not know for sure if our additions are sound or not, and until we know, the dependable types extension might not be really suitable for proof carrying code.
A compromise solution would be starting from something like rustbelt/oxide or patina (whichever easier to work with / close to completion) and model the (yet to be designed) dependable type extension there and then we know high confidence that it work, but I am not sure if any of the 3 projects completely model the rust language.
I am looking for your input on the matters, If I am lucky and can come up with a clear objective, I might be able work on that project for some time.