HVM icon indicating copy to clipboard operation
HVM copied to clipboard
verified publisher icon HigherOrderCO

Formally Verified Implementation

Open enricozb opened this issue 1 year ago • 0 comments

At some point we should write a formally verified implementation of the HVM specification.

We should then use this as the reference implementation.

This implementation could also be done in a DSL that transpiles to the other (C, Rust, CUDA, maybe more) runtimes. It is unclear, however, how to ensure that this transpilation is also formally correct.

CompCert famously did something similar by formalizing a compiler for a very large subset of the C11 standard.

enricozb avatar May 21 '24 07:05 enricozb