Proof-Caring Code

Design by Contract, Meet Symbolic Execution!

So I have this idea of using Design by Contract for the C language in a kind of (open!)synergy with Symbolic Execution based on KLEE. 

The idea is that instead of testing, you write (or even better, generate!) symbolic verification "drivers" for your APIs based on their contracts (preconditions and postconditions/return values for now). Briefly, the function preconditions should imply the postconditions (given the actual code).

Because this approach aims to replace testing to a large degree, what better way to present it in a developer-friendly manner than using test-like koans as an inspiration? You know, as previously done here for Ruby, and for many other languages, as a way to learn languages and-and-by TDD.

For now, check this: https://github.com/cornelizbasa/koan-tracts

Instead of having tests fail, you'll be presented with assertion violations accompanied by counterexamples produced by KLEE, such as: http://pastebin.com/4zQhV1Rn.

More stuff coming soon.

P. S. The title is a play (or troll, if you prefer) on proof-carrying code (PCC). Because this approach will just need the contracts, not the proof inside the code, so instead of "carrying" the proof, it just "cares" about it being feasible through KLEE ;-)