On 17 January 2011 14:59, Jure PeD ar <[email protected]> wrote: > Hello all, > > I've recently watched this talk from 27c3: > http://media.ccc.de/browse/congress/2010/27c3-4123-en-defense_is_not_dead.htm l > > Very well spent hour. > > I assume that since OpenBSD's crowd main goal is security, some of you > might have considered using such techniques to improve the critical pieces > of your code. Since these techniques are not in widespread use over the > OpenBSD code base I also assume that you have some decent arguments against > their use. > > I understand there are lincensing issues (nonfree nature of microsoft vcc > and french compcert), but putting these aside, what are your > practical/technical reasons for not using them? > >
Isn't formal verification of code one of those academic-impossible-to-do-in-real-world thing ?
