Proofs about the correctness of C code are now much easier. There is a software tool chain using "Verifiable C" to make systems safer.
Here is a tutorial on it, and general proof code writing. It is fully verified in Coq.
@jmw150 great link in general, thanks for sharing. I learned a bit of Coq during an undergrad logic course and a Haskell course. Reading the titles and contents of the other books in the series vaguely triggers some memories although in reality I'm pretty sure I've forgotten most of it. Sometimes, I wish I could focus more on formal systems but the problem is that in my head I need to be able to see tangible results relatively quickly to keep engaged with something which is why I lean more towards embedded systems and ML rather than more theoretic aspects of SWE like formal validation and proofs. Nonetheless, I can appreciate it from a far as a very fascinating field.
@zpartacoos you may like recent work in programming synthesis then.
Right now it is an area where computational logic and machine learning meet. The advantage is more modularity and control. I think as ml gets bigger it will start merging more with formal systems for sake of scalability.
