<div dir="ltr">David,<div><br></div><div>Interesting idea! I can think of two challenges; one is the sheer scale of most kernel codebases (eg, the ACIS binaries are around 100 mb). The other is that writing the specification for a kernel would itself be a significant task and at least at first glance would have to make heavy use of rich, dependent types. The state of a geometric program that has 'gone wrong' seems much harder to encode than a null pointer dereference. </div><div><br></div><div>I wonder if there is a way to scope down the surface area that would need to be formally verified to still have a significant impact on the development of a rich kernel. At least a few folks are investigating this: <a href="http://www.researchgate.net/publication/221610369_A_Formally_Verified_Geometric_Modelling_Core">http://www.researchgate.net/publication/221610369_A_Formally_Verified_Geometric_Modelling_Core</a> , but I'm not aware of any broad uptake or reusable components that have been verified. </div><div><br></div><div>Andrew</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Nov 8, 2015 at 5:13 PM, David Kaufman <span dir="ltr"><<a href="mailto:davidgilkaufman@gmail.com" target="_blank">davidgilkaufman@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">My understanding from our discussion last week is that writing a B-Rep<br>
kernel is difficult primarily because there are tons of edge cases for<br>
how objects can intersect each other and it's really hard to get them<br>
all correct/test for all of them. If this is the main challenge then my<br>
intuition is that it would be best solved by building a formally<br>
verified b-rep kernel (and that perhaps it would take much less time to<br>
write that way). Do any of you know if anyone has tried to write a<br>
formally verified b-rep kernel or why not?<br>
</blockquote></div><br></div>