I am somewhat familiar with Daniel J. Bernstein, but you'll have to enlighten me on why you've brought him up. If you're referencing programs where half the so

I am somewhat familiar with Daniel J. Bernstein, but you'll have to enlighten me on why you've brought him up. If you're referencing programs where half the source code is written in a theorem proving language like CoQ, that's not really "written in C", now is it?