I didn't mention rust. If you were targeting something that only has a c compiler and it is critical infrastructure, f* could prove correctness and then generat

I didn't mention rust. If you were targeting something that only has a c compiler and it is critical infrastructure, f* could prove correctness and then generate c from that as an ir. A lot of safety crtical stuff uses a DSL to generate c that humans don't touch afterwards.