Comment by anon291

I'm about as into formal methods as you can get, with a deep background in Haskell and such. Rust is wonderful and all that, but sometimes I think the optimism is misplaced and doesn't come from a place of full knowledge. Statements like this make me scared:

> The geometry engine is manifold, which guarantees watertight meshes from boolean operations. The Rust bindings give us zero-cost abstractions over the C++ core — the operator overloads compile down to direct manifold calls. No garbage collection pauses. No floating point surprises from a scripting layer.

Floating point is incredibly surprising. People seem to believe that a typed programming language eliminates floating point error. Scripting and interpretability has nothing to do with why floating point is hard. Floating point arithmetic is as deterministic in Python as C++ or Rust. The issue is whether people understand the rules. The type system has nothing to do with this, as floating point errors are almost always value errors, not type errors. The only way to avoid floating point errors using formal methods is an actual theorem prover. Rust is nowhere close to being a theorem prover.