<div dir="ltr"><div>This is a wonderful discussion, David!</div><div><br></div><div>If we are only looking to verify topological correctness, the Euler Operators provide the necessary tools to maintain the Euler Characteristic with every topology change. Mårtti Mantyla's excellent book, "Introduction to Solid Modeling", discusses this topic in depth. </div><div><br></div><div>The space of topologically-correct models, however, is extremely large in comparison to the space of topologically-correct, geometrically-correct (e.g. non-self-intersecting, non-negative volume) models. Geometric correctness checks appear to be the "magic" of implementing such a kernel. I would be surprised (and delighted!) to see a proof-based system capable of reasoning about a comparably complex issue.</div><div><div><br>Furthermore, we are typically limited to fixed-precision arithmetic for operations that require infinite precision. This has a multiplicative effect on the complexity of implementing, e.g. boolean operations. We might say that we could use rational arithmetic to represent all geometry, but I think this rapidly limits us to simple surface and curve representations (like lines and planes). </div><div><br></div><div>I should say that I'm very interested to see a system that combines the control that comes with free-form surfaces and the simplicity of verification that comes with a simplified geometric representations.</div></div><div><br></div><div>On a side note, I wouldn't suggest we use the size of the ACIS binaries as a heuristic for the complexity of implementing a kernel. There are so many years of development in that system and it has not been developed with an intent to minimize the size of the kernel. You might also find that the core libraries are rather small in comparison to the entire system.</div><div><br></div><div>~Peter</div><div><br></div><div><br></div><div><br></div><div><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Nov 9, 2015 at 4:12 PM, Andres Erbsen <span dir="ltr"><<a href="mailto:andreser@mit.edu" target="_blank">andreser@mit.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
Quoting Andrew Zukoski (2015-11-08 20:27:33)<br>
<span>> Interesting idea! I can think of two challenges; one is the sheer scale of most<br>
> kernel codebases (eg, the ACIS binaries are around 100 mb). The other is that<br>
> writing the specification for a kernel would itself be a significant task and<br>
> at least at first glance would have to make heavy use of rich, dependent types.<br>
> The state of a geometric program that has 'gone wrong' seems much harder to<br>
> encode than a null pointer dereference. <br>
><br>
> I wonder if there is a way to scope down the surface area that would need to be<br>
> formally verified to still have a significant impact on the development of a<br>
</span>> rich kernel. At least a few folks are investigating this: [1]http://<br>
> <a href="http://www.researchgate.net/publication/" rel="noreferrer" target="_blank">www.researchgate.net/publication/</a><br>
<span>> 221610369_A_Formally_Verified_Geometric_Modelling_Core , but I'm not aware of<br>
> any broad uptake or reusable components that have been verified. <br>
<br>
</span>I will comment on the two challenges in the opposite order: starting<br>
with specification and moving on to proof engineering.<br>
<br>
Disclaimer: I do not know much about B-rep cad implementation internals;<br>
I am also a firm believer in the utility of formal verification.<br>
<br>
If the issue is computing a representation of the intersection (resp.<br>
union) of two objects represented using B-reps, then here is a possible<br>
specification for that: a point is inside the output object iff it is in<br>
both (resp. either) of the input objects. I am assuming defining when a<br>
point is inside an object is not hard (e.g., a ray from that point<br>
intersects with the surface some odd number of times).<br>
<br>
I am not saying that all operations will be that easy to specify (or<br>
even that this specification is sufficient for all needs), but I am also<br>
optimistic that verifying similar sanity properties can be helpful in<br>
improving the reliability of the software.<br>
<br>
Generalizing from there, the operations supported by both B-reps and<br>
F-reps can quite meaningfully be verified by proving that they are<br>
equivalent: if F1, F2 and B1,B2 represent the same objects (as F-reps<br>
and B-reps respectively), then f_B(B1,B2) represents the same object as<br>
f_F(F1, F2). This of course does not help you any if the operation is<br>
hard to define in one of the representations.<br>
<br>
The cited paper is based on a methodology from two decades ago,<br>
implemented using tools from 10 years ago. I would expect that today's<br>
proof automation can scale up from this (20 years ago it was news to<br>
verify a small finite state machine, now there are verified web servers,<br>
OS kernels and quadcopter controllers). Which is not to say that it is<br>
trivial to do or does not require expertize; yet I continue to be<br>
optimistic.<br>
<br>
And this leads us to what I think is the main thing that makes<br>
verification hard: the lack of a "standard library" of verified<br>
primitives, be they geometric or algorithmic. Often it has not been the<br>
complexity of the algorithm or the elusiveness of the specification that<br>
has left good software unverified, it is that the path of least<br>
resistance towards the next product/paper is to use readily available<br>
non-verified building blocks instead of spending more time on creating<br>
verified equivalents. In which cases this greedy approach actually saves<br>
net time (after accounting for debugging/support/disaster management and<br>
such) is a very open question.<br>
<br>
I think that verifying the fundamental operations that "everything else"<br>
depends on is quite often a good idea, especially they are notorious for<br>
being prone to implementation error. The common subset of F-rep and<br>
B-rep operations is one possible choice of this core. Yet the practical<br>
utility of verifying this obviously depends on what kind of expertize<br>
the people working on this will have and how much the correctness of the<br>
core actually matters (i.e., if it is wrong, how much money/time is<br>
lost).<br>
<br>
Those are my two cents.<br>
<br>
Best,<br>
Andres<br>
<br>
><br>
> Andrew<br>
><br>
><br>
> On Sun, Nov 8, 2015 at 5:13 PM, David Kaufman <[2]<a href="mailto:davidgilkaufman@gmail.com" target="_blank">davidgilkaufman@gmail.com</a>><br>
<span>> wrote:<br>
><br>
> 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>
><br>
><br>
><br>
</span>> References:<br>
><br>
> [1] <a href="http://www.researchgate.net/publication/221610369_A_Formally_Verified_Geometric_Modelling_Core" rel="noreferrer" target="_blank">http://www.researchgate.net/publication/221610369_A_Formally_Verified_Geometric_Modelling_Core</a><br>
> [2] mailto:<a href="mailto:davidgilkaufman@gmail.com" target="_blank">davidgilkaufman@gmail.com</a><br>
</blockquote></div><br></div></div>