adyavanapalli
Joined 9 years ago
Karma
266
Submissions
85
Member since
Feb 9
I like math and the stars.
View on Hacker NewsRecent submissions
Comment · 8 days ago
The account now holds about $1k USD. A second deposit landed in the account about 7 minutes ago from when I posted this comment.
EDIT: Now worth $2k
Comment · 8 days ago
Two days ago, Anthropic published an article about formally verifying software and producing something like 180 million lines of Rocq in just a couple of weeks. I think build and formally verifying an entire OS kernel might be within its reach in a couple of months.
Comment · 9 days ago
I don't understand why this is even a problem. If current models can formally verify vast amounts of software, couldn’t you use it to build a sandbox with formally verified guarantees against leaks?
Comment · 10 days ago
> Claude can write a proof showing that a compiled program’s behavior satisfies the requirements of a formal spec (which is verified by an external proof checker). However, a proof checker can’t tell you whether your spec matches reality.
Imagine having a formal spec for reality!
Comment · 1 month ago
As the saying goes, those who know don't say and those who say don't know.
Comment · 3 months ago
This is actually brilliant. I've seen other approaches where the context is selectively pruned, but never in a recoverable way.
P.S. Love the "bonsai" name btw!
Comment · 3 months ago
Honest question, but since when were biographies ever _authorized_? I would assume you would simply inform the subject out of politeness if at all.
Comment · 3 months ago
This is soooo incredibly cool. Beyond the Tom Riddle diary aspect, I love the idea of this as a new medium for interacting with an LLM. You could gift it to someone and they could just write naturally, their thoughts, questions, notes, and get responses back without typing or speaking. It feels less like a chatbot and more like a journal you can communicate through. You could give it a personality and all.
Comment · 4 months ago
For the edit tool, you should consider implementing a hash-based approach where each line of code is hashed and referenced by it when doing replacements. You can read up on the approach here: https://blog.can.ac/2026/02/12/the-harness-problem/
I didn't do much benchmarking, but anecdotally, I found it to be making less edit errors. YMMV
Comment · 5 months ago
What you're talking about is so extremely rare that it's much more likely that the entire Earth is destroyed by an asteroid right this inst...
Comment · 6 months ago
What are the numbers you are getting?
Comment · 6 months ago
I had a chance to look at this and noticed you were sending telemetry to an endpoint you control: https://dirac.run/v1/event. It doesn't seem like you're sending anything obviously sensitive or doing anything in bad faith (though, I do see api errors being sent, which could potentially leak sensitive info), but you gotta admit that that's scary seeing you as the sole dev for this. Plus, it's opt out too. Sorry, it's no go for me.
Comment · 6 months ago
I haven't tried it, but I'm curious why you decided to implement a whole new harness over just writing extensions in pi. From whatever I've done with pi so far, the extension api is quite extensive. Hash anchored edits, for example, can definitely be implemented in pi. Anyhow, thank you for showing us your project and will be checking it out later. Cheers!