Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

github.com

Post reply on HN
Print view View original

41–50 of 57 posts

Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

#41

Post by 1bpp »

iFire wrote: post #10
bob1029 wrote: post #6

This is really neat. I think CSG is one of the more intuitive ways to build 3d environments (especially 'indoor' ones). No geometry is ever destroyed in a proper CSG workflow. A hierarchy of brushes makes it possible to very rapidly iterate parameters like how long a hallway is or the time it takes to get from one objective to another. Often, you only have to apply a transform to a single brush to affect something th…

That's why I integrated manifold into godot engine for constructive solid geometry! https://github.com/godotengine/godot-proposals/issues/9711

Thank you! CSG has made level prototyping more fun and fast in Godot for me.

Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

#42

Post by permute »

_bent wrote: post #40

Would you still be able to deal with coplanar faces if you were to expand this to floats?

We could use floats internally and gain a lot of performance as I described in my response here: https://news.ycombinator.com/item?id=49085136. With this we would still be able to handle special cases correctly.

If you mean, you want float in the interface, I think the picture would be the similar as I described there: You still need to fallback to higher precision for certain computations. But you would also not be able to return the outputs correctly, so we would need to think about how we want to describe this in the specification...

Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

#43

Post by amuresan »

permute wrote: post #33
swiftcoder wrote: post #22

Ok, that's very cool. I don't yet grasp exactly how this deals with numerical stability - the one true enemy of mesh-based CSG operations

The implementations uses exact rationals numbers. So there are no issues with numerical errors. We can do all geometrical operations exactly. Many performant implementations have a separate layer that tries to use floats to decide inequalities and fall back to higher precision when floats are not sufficient. As I understand, this layer can be separated from the geometrical predicates we need (what I mean by predicate…

Moving to exact predicates on top of floating point numbers would be a big speed boost. CGAL does this.

Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

#44

Post by iFire »

regularfry wrote: post #31
bartvk wrote: post #14

Congrats with this achievement. Do you see it possible that this project can be integrated into, for example, FreeCAD?

CSG on meshes isn't really where FreeCAD struggles or focuses. That's more BRep, which is a harder problem than CSG. Blender used to struggle with boolean operations, though. Seems to have got much better some time in the last couple of years, but without knowing any of the backstory I don't know if they've bodged it into shape or would benefit from something proven.

Blender uses the manifold library after years of petitioning

Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

#45

Post by newobj »

swiftcoder wrote: post #22

Ok, that's very cool. I don't yet grasp exactly how this deals with numerical stability - the one true enemy of mesh-based CSG operations

Came here to ask about this too. I was doing CSG stuff in the early 2000's and got physically and mentally sick from the pure hell that floating point accuracy created for me. Literally led me to quit my job. Full crashout. iykyk

Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

#46

Post by outoftheweed »

no lean background here so the proofs are over my head, but the framing makes sense to me. everything i've shipped that claude co-wrote, the thing that made me trust it was running it end to end, never reading it. having a checker do that part is a way better deal.

Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

#47

Post by angry_octet »

ekidd wrote: post #26
angry_octet wrote: post #24

Earlier quoted context omitted.

The code generation for Lean is not AFAIK verified in any way. It uses C as a portable assembler, and uses too many fancy C constructs to be compiled by CompCert C, which is the only fully verified compiler. So you can have the strange situation of proof that the Lean code is correct, but no way of proving that the running machine code corresponds with the same program. There is also the problem of knowing whether th…

Still, this is not a bad situation overall. If you are forced to trust the C compiler to correctly compile C, and the hardware to correctly implement the instructions in the documentation, well, you're already forced to trust both of those every day. So this doesn't give you an absolute proof of correctness. But it does substantially reduce the size of the problem, which is now limited to (1) verifying that you actua…

Oh yes, it is still a better situation. Although C compilers are quite buggy.

Since Lean can emit LLVM it might be more achievable to reach performant assembly without going via C. All sorts of interesting work in progress.

https://dl.acm.org/doi/10.1145/3192366.3192377

(I am rate limited to ~5 comments a day so not replying for ages is just a function of the HN gods on Mt Sunnyvale.)

Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

#48

Post by kens »

angry_octet wrote: post #24
brandonpelfrey wrote: post #18

This seems like very cool work. I'm sorry if I missed it: I'm still not sure how we go from verified proof (Great!) to an implementation (by LLM or by Human) which you're sure actually conforms to the proof? How do we know that the implementation maps precisely to the description within the proof?

The code generation for Lean is not AFAIK verified in any way. It uses C as a portable assembler, and uses too many fancy C constructs to be compiled by CompCert C, which is the only fully verified compiler. So you can have the strange situation of proof that the Lean code is correct, but no way of proving that the running machine code corresponds with the same program. There is also the problem of knowing whether th…

It's kind of hopeless to try to prove that a microprocessor works according to spec, since you're dealing with physical objects in the real world. For instance, early versions of Intel's 386 processor had a 32-bit multiply problem that only showed up in some chips under particular combinations of temperature, voltage, and frequency, probably due to a transistor that wasn't large enough to provide an electrical margin under worst-case conditions.

Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

#49

Post by agentultra »

saithound wrote: post #39
agentultra wrote: post #28

Earlier quoted context omitted.

Right, I’m thinking of the de Bruijin criterion applied to the generated kernel in this case. That generated kernel sounds large, and being generated, I’m curious as to why or how we don’t have to verify/understand it?

You're confused because the word kernel is used in two different senses. The "generated kernel" refers to a "geometric modeling kernel", which has absolutely nothing to do with the proof-checking kernel that the de Bruijn criterion talks about. The proof can be verified by Lean's ordinary proof-checker, or external checkers.

Okay so in the sense of Lean’s kernel, we can trust it as long as we understand it. Verifying it cannot be automated therefore, according to the criterion, it must be small so that it can be verified by a human.

Does it not also follow that we should also understand the geometric kernel using a similar criterion or, what I’m trying to understand, is there a mechanism in play in this project that verifies it for us automatically so that we only need to understand the specification and can trust the generated parts?

There are some pointers to answer this question myself that I’m looking into. Neat stuff.

Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

#50

Post by UltraSane »

agentultra wrote: post #49
saithound wrote: post #39

Earlier quoted context omitted.

You're confused because the word kernel is used in two different senses. The "generated kernel" refers to a "geometric modeling kernel", which has absolutely nothing to do with the proof-checking kernel that the de Bruijn criterion talks about. The proof can be verified by Lean's ordinary proof-checker, or external checkers.

Okay so in the sense of Lean’s kernel, we can trust it as long as we understand it. Verifying it cannot be automated therefore, according to the criterion, it must be small so that it can be verified by a human. Does it not also follow that we should also understand the geometric kernel using a similar criterion or, what I’m trying to understand, is there a mechanism in play in this project that verifies it for us au…

The geometric kernel is written in Lean and is thus also verified by the Lean prover.
Post reply on HN