HN user

dnmc

66 karma

I write code at Google. Opinions are my own. https://github.com/dmcardle

Posts1
Comments16
View on HN

This has been on my mind lately! Especially in light of the many incomprehensible but machine-checkable proofs we've been hearing about.

Occam's Razor is a useful heuristic, but it biases us towards simpler explanations.

When you have two monitors, is your head always turned to one side? That always hurts my neck, so I wind up with the second monitor relegated to the side, where I never actually look at it.

There are languages like Dafny that permit you to declare pre- and post-conditions for functions. Dafny in particular tries to automatically verify or disprove these claims with an SMT solver. It would be neat if LLMs could read a human-written contract and iterate on the implementation until it's provably correct. I imagine you'd have much higher confidence in the results using this technique, but I doubt that available models are trained appropriately for this use case.

Maybe this isn't what you're suggesting, but it's already possible to make an interface that prevents callers from doing math on indices in Rust — just return a struct that has a private member for the index. The caller can pass the value back at which point you can unwrap it and do index arithmetic.

And If `jj absorb` gets it wrong, you can run `jj undo`.

This is such a killer feature to me. I'm not scared to start potentially gnarly rebases anymore because I can painlessly undo.

I don't think the OP ever returned with a conclusive answer, but I'm somewhat convinced by the commenters that it was either a low-frequency engine sound rattling the neighbor's windows or something to do with the car's rear-cross sensor.

Oh no! I can run it on my phone, which is a few years old, so I figured it wouldn't lock anybody's computers up.

It's pretty CPU-heavy because it's constantly creating and updating SVG elements. I may attempt to rewrite sometime with WebGL and shaders :)