Re:On the history and justification of the C programming lan...
by nickpsecurity on Thursday August 18, 2016 @05:20PM
(#12316405)
I just got a bunch of papers on first-order verification, implementation, compilers, and so on as the simplicity & tractability part peaked my interest. I'm keeping them in case I run into some students or hobbyists that want to try that on top of some "verify the verifier" kind of issues. Then I see these suggestions...
"(0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas.
(1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice."
I'll add those to the list given that sounds worth a good try. Especially if combined with automated approaches to generating & solving for common attributes like in SPARK and AutoCorres. Maybe something will come of it.
"(0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas.
(1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice."
I'll add those to the list given that sounds worth a good try. Especially if combined with automated approaches to generating & solving for common attributes like in SPARK and AutoCorres. Maybe something will come of it.