I feel like this kind of intensely provably-correct language (this one, Coq, Agda, etc.) isn't so much for writing whole programs in, as for writing the small, very-important-to-verify modules, that will link with other, less important modules to form a whole program.
When you're writing provably-correct "error kernels"[1] for your software, you probably want as little interaction with the OS to happen inside the kernel as possible. Write the rest of your program in a glue language, then hand off to the proven-correct error kernel for the hot loop. Probably over stdio, or transactional SHM IPC, or any other mechanism like that that has as little failure-surface as you can get away with.
When you're writing provably-correct "error kernels"[1] for your software, you probably want as little interaction with the OS to happen inside the kernel as possible. Write the rest of your program in a glue language, then hand off to the proven-correct error kernel for the hot loop. Probably over stdio, or transactional SHM IPC, or any other mechanism like that that has as little failure-surface as you can get away with.
[1] https://medium.com/@jlouis666/error-kernels-9ad991200abd