#proofs #dependent #author #matt #ghosts #departed #noonan

dependent_ghost

An implementation of Matt Noonan's 'Ghosts of Departed Proofs'

2 releases

0.1.1 Jul 19, 2020
0.1.0 Jul 19, 2020

#1475 in Rust patterns

MIT license

9KB
147 lines

What is this?

dependent-ghost is a library that provides some of the benefits of dependent typing to Rust via the Ghosts of Departed Proofs technique. Library authors can provide APIs with statically-checked preconditions and invariants, which the user can validate however necessary.

All credit for this technique goes to Matt Noonan, the author of the original paper.

No runtime deps