Hi Andrés,
I'm not Andrew, but this
question fell directly into one of my ongoing research themes, so here
are my 2 cents. Also this looks unrelated to Andrew's post about consulting contracts, so I split it off into a separate topic.
Our work on the PGo compiler (
https://github.com/DistCompiler/pgo)
is quite similar to what you ask. We aimed to take PlusCal and build
(at least plausibly) production-capable distributed systems with it. Key
challenges that make this non-trivial are things like disjunctions
(when not in a model checker, you need to figure out which branch to
run), and representing native API calls (which can do things like
temporarily fail, time out, signify you should go back and try a
different branch of your disjunction). Our paper (free link at my
website
https://fhackett.com/files/asplosb23main-p12-p-e73de3693c-62943-final.pdf) explains this to the extent possible in ~12 pages; feel free to follow up if you are curious about something we don't cover.
Also, it's worth mentioning a similar effort to convert PlusCal to Erlang, called Erla+ (
https://github.com/mmhristov/Erlaplus;
they link a paper and talks also). It converts into Erlang, and makes
different tradeoffs to PGo. In exchange for sacrificing some generality,
they can generate much more "normal" code (look at PGo's generated
Go... it's completely inhuman, and due to its need to be general, it can
do "stupid" things a human would know to avoid).
To
talk about your specific question, honestly if you can solve it for Go /
Erlang, you can solve it for C. It might be incomprehensible C full of
reference counting / tricky memory management, non standard data
structures, and unintuitive control flow. One unique challenge for C is
that the C runtime lets you do a lot of bad stuff without even an error
message, so you'd have to try harder to debug and validate your
translator (and/or its output C code).
Aside: for performance tuning of general purpose translated code, that's an open
problem which I aspire to address (results TBD). We found all general purpose translator attempts in this domain can be multiple times slower than hand written code, so far at least (see our paper above). If you want something practical right now, look at things like F*, which at the expense of a lot of dev time (completely different model for verification, more involved), has been successfully used for some cool low level encryption libraries (ref:
https://project-everest.github.io/). See also Rust tools like Verus and Prusti.
I hope this helps.
Best,
-Finn