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/Pape

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-esop07.pdf https://people.eecs.berkeley.edu/~necula/Papers/deputy-esop0...