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.

softwarefoundations.cis.upenn.

@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.

Follow

@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.

Sign in to participate in the conversation
Qoto Mastodon

QOTO: Question Others to Teach Ourselves
An inclusive, Academic Freedom, instance
All cultures welcome.
Hate speech and harassment strictly forbidden.