4 ms·

How does it compare against https://github.com/elalish/manifold https://github.com/elalish/manifold in performance and zero corruption? I spent a lot of time m

by iFire 2mo ago

How does it compare against https://github.com/elalish/manifold https://github.com/elalish/manifold in performance and zero corruption? I spent a lot of time making elalish/manifold work in Godot Engine and it is now a method in Blender too. https://manifoldcad.org https://manifoldcad.org If it helps, feel free to use the apache2 licensed unit tests that were generated in manifold development https://github.com/elalish/manifold/tree/master/test https://github.com/elalish/manifold/tree/master/test

iFire 2mo ago
> Why we cannot have manifold output meshes in general As far as I know manifold is not verified software, but it does promise that manifold inputs become manifold outputs. I wonder how manifold will break in that condition or would it snap to the nearest manifold. https://github.com/schildep/verified-3d-mesh-intersection#why-we-cannot-have-manifold-output-meshes-in-general https://github.com/schildep/verified-3d-mesh-intersection#wh...
- iFire 2mo ago
  On a readme style note, please spend more time explaining the algorithm and less time bragging on how amazing vibe coding is or how Lean has a zero trust proof. I presume the new advance is claim that verified-3d-mesh-intersection is verified and not the claim that vibe coding can replace hand proofs or that the claim that lean4 can be correct without trusting llms.
- elalish 2mo ago
  The difference is that my Manifold library uses a different definition of what constitutes a manifold mesh: https://github.com/elalish/manifold/wiki/Manifold-Library#manifoldness-definition https://github.com/elalish/manifold/wiki/Manifold-Library#ma.... By being a purely topological definition, there is no implicit assumption that vertices with the same coordinates are connected. As such we can still generate a 2-manifold even in the "impossible" cases. The more important difference though, is that our library can still handle epsilon-valid self-intersecting meshes, rather than just reporting an error. This is critical in practice because meshes are stored, transported, and transformed in floating-point, so even the formally-proven non-self-intersecting results of the library under discussion will not necessarily be valid input for it anymore after a round-trip through a file format or a rotation. Still, these are details. I think the real contribution here is demonstrating a new approach to formally verifying software even for notoriously difficult problems. I believe that concept is really important, as the general state of software reliability tells me that the state of the art in testing software is desperately lacking. I think formal verification may well be one of the most important aspects of computer science research in the nearish term.
permute 2mo ago
The runtime performance is most probably worse than yours. The goal of this project is a minimal specification that a reviewer can trust. See section in readme on performance and how it could be improved while still keeping formal guarantees, but would mean a reviewer having to trust axioms on floating point numbers: https://github.com/schildep/verified-3d-mesh-intersection#performance https://github.com/schildep/verified-3d-mesh-intersection#pe...

by iFire 2mo ago

iFire 2mo ago

> Why we cannot have manifold output meshes in general As far as I know manifold is not verified software, but it does promise that manifold inputs become manifold outputs. I wonder how manifold will break in that condition or would it snap to the nearest manifold. https://github.com/schildep/verified-3d-mesh-intersection#why-we-cannot-have-manifold-output-meshes-in-general https://github.com/schildep/verified-3d-mesh-intersection#wh...

iFire 2mo ago
On a readme style note, please spend more time explaining the algorithm and less time bragging on how amazing vibe coding is or how Lean has a zero trust proof. I presume the new advance is claim that verified-3d-mesh-intersection is verified and not the claim that vibe coding can replace hand proofs or that the claim that lean4 can be correct without trusting llms.
elalish 2mo ago
The difference is that my Manifold library uses a different definition of what constitutes a manifold mesh: https://github.com/elalish/manifold/wiki/Manifold-Library#manifoldness-definition https://github.com/elalish/manifold/wiki/Manifold-Library#ma.... By being a purely topological definition, there is no implicit assumption that vertices with the same coordinates are connected. As such we can still generate a 2-manifold even in the "impossible" cases. The more important difference though, is that our library can still handle epsilon-valid self-intersecting meshes, rather than just reporting an error. This is critical in practice because meshes are stored, transported, and transformed in floating-point, so even the formally-proven non-self-intersecting results of the library under discussion will not necessarily be valid input for it anymore after a round-trip through a file format or a rotation. Still, these are details. I think the real contribution here is demonstrating a new approach to formally verifying software even for notoriously difficult problems. I believe that concept is really important, as the general state of software reliability tells me that the state of the art in testing software is desperately lacking. I think formal verification may well be one of the most important aspects of computer science research in the nearish term.

permute 2mo ago

The runtime performance is most probably worse than yours. The goal of this project is a minimal specification that a reviewer can trust. See section in readme on performance and how it could be improved while still keeping formal guarantees, but would mean a reviewer having to trust axioms on floating point numbers: https://github.com/schildep/verified-3d-mesh-intersection#performance https://github.com/schildep/verified-3d-mesh-intersection#pe...