Goodbye C developers: The future of programming with certified program synthesis

submited by

Style Pass

2021-07-05 07:30:05

A nother day, another dime, another Major. Security. Vulnerability. All caused by stubborn C developers refusing to abandon their outdated programming language.

But wait! I hear you cry, the C-programming language forms an integral part of the foundations of our ecosystem; countless billions of lines of C code underlie much of the technology that upholds our modern society.

Who else but these masters of code, these witches and wizards of the wire, these lords of low-level coding could we trust to write this code?

Note: To be clear, this post isn't in advocacy of a copy-and-paste statistical approach to code generation with no guarantees of correctness (like the recently released Copilot), but rather a semantic-aware certified synthesis that produces correct code 100% of the time

Surely, that's not too hard to understand? After all, it's just a bit of pointer twiddling, a malloc or two, and a single recursive call - what could be more simple?