[uecker]

I have plan to do just this. See N3211 and N3395 for an initial sketch.

https://www.open-std.org/jtc1/sc22/wg14/www/wg14_document_lo...

[anqurvanillapy]

Cool, and the paper mentioned in the document "Dependent Types for Low-Level Programming" [1] is such a gem.

[1]: https://people.eecs.berkeley.edu/~necula/Papers/deputy-esop0...