> For hardcore security jobs I still use Ada, for (rare) GUI jobs I still use > FreePascal, for pure crypto jobs like porting or optimizing crypto algos I > still use C along with formal modelling, proto verif. and formal (usually > static) analysis.
Extremely interesting! Could you give a list of your C formal modelling toolkit / workflow ? And a hint about what kind of common things it flags in Nim generated C code? Also, since you mentioned using formally verified C for crypto work - is there anything helping with verifying constant time stuff? How useful is everything given that anything practical uses a non-verified compiler somewhere along the high-level -> machine code path?
