alt Hacker NewsBeen doing this at work for the past couple weeks. Extremely powerful to be able to have an agent open a PR with some experiments showing it makes some function faster using SIMD or CUDA, and just confidently merge it because the PR has a Rocq proof that it's behaviorally equivalent to the original implementation.
Replies
hedgehog • today at 1:14 AM
I'm curious about your workflow (or the one in the blog post), I have been doing some experiments proving things about existing binaries and it's been extremely slow progress.
➕ show 1 reply
How do you gain confidence that your theorem actually applies to your code?