HNHacker News
TopNewBestAskShowJobs

yazaddaruvala

3,325 karma · joined May 31, 2013

submissionscomments
yazaddaruvala··on LLMs are making formal software verification feasible at a much larger scale
Rust is great! No two ways about it.

What I want tho would be Rust+Akka for example. There has to be a distributed execution mechanism that is as seamless as Java’s GC. Then the distributed execution mechanism needs to evolve to also be as light weight and “zero cost” while being seamless like Rust’s compile time memory management.

yazaddaruvala··on LLMs are making formal software verification feasible at a much larger scale
These are the good good questions. I wish I was smart enough to answer them.

I think the best bet is to let a hundred developers play at it for a bit. There will be a lot of bespoke domain specific declarative languages. They will over time learn from each other to be better and better.

Experiments like GoogleSql’s pipe syntax https://docs.cloud.google.com/bigtable/docs/reference/sql/pi... getting pushed even further and further. That’s where I’d put my money. Cloudflare might be another candidate for building such a programming language for the distributed compute and memory “machine”.

(Also once we are there) I think there will be even better questions: What does programming CRDTs like a blockchain that reconcile across Mars and Earth look like? and in that way, LLMs will constantly be useful helpers to explore the state/latent space.

yazaddaruvala··on LLMs are making formal software verification feasible at a much larger scale
We don’t need “a declarative language flexible enough to do what an imperative language is capable of”

We need “a declarative language flexible enough to do what the product requires”

yazaddaruvala··on LLMs are making formal software verification feasible at a much larger scale
``` SELECT A, B, Sum(C) FROM Somewhere GROUP BY ALL ```

Very few developers look at the underlying “source code” that this SQL compiles into. Very few people even read the “source code” that tsc outputs.

The reality is the lowest level checkpoint worth looking at and understanding is the highest possible abstraction layer which preserves 100% of the needed precision and flexibility that the product being built requires.

Also, you’d just use something like sscache or just .o files to speed up compilation. It’d be unusual to store compiler MIR/LIR in git.

I think the important part will be figuring out what we need from the higher level language that achieves 100% of the precision and flexibility of Rust for the product being built.

yazaddaruvala··on LLMs are making formal software verification feasible at a much larger scale
AGI will accelerate it, but way before agentic development I learned this was the future when I worked at Amazon. I no longer have access to the internal talks about it (amazing to watch) but here is a public link worth reading:

https://aws.amazon.com/blogs/storage/how-automated-reasoning...

yazaddaruvala··on LLMs are making formal software verification feasible at a much larger scale
I think somewhat of the opposite will actually occur. LLMs won’t formally verify LLM generated imperative style code. We (including agentic development) will move on from imperative languages, skipping functional and move to deterministic declarative languages.

Likely, a proliferation of experimental languages all somewhat akin to Typescript for SQL with significantly more nuanced operators to tersely capture the same outcomes as imperative languages.

They’ll compile down to be able to run performantly for game development or even for the Linux kernel (as if Linus would ever agree lol) but also they’ll be able to run on distributed execution engines with effectively a shared memory space, etc.

Allows for significantly more terse artifacts. Lower chance of hallucination, fewer output tokens, fewer thinking loop iterations and concise enough for humans to review (for domains that need it).

On top of that, additional theorem like syntax to drastically limit the ability of functions, etc. likely some sort of higher level effect system for verification. Used for many things like “constant time compilation for crypto functions”, and also “ensure acid compliance” for writes and reads in a local context, and things like “ensure only once delivery” for functions on a distributed execution engine.

At which point every program will be formally verified by default. You could think of it as AdaErlangSQL+++

yazaddaruvala··on After Math
Oh wow, that’s a lovely way to say it!

Purpose rebirth is the re-finding of play in the thing we choose to partner with AI (likely with a paycheck attached) to do N hours a week.

yazaddaruvala··on After Math
I like that!
yazaddaruvala··on After Math
I hope one day I can re-earn it. All the best!
yazaddaruvala··on After Math
Yes, I am making up a narrative. That’s why I used words like “postulate”, “think”, “I wonder”, and “I may be wrong”.
yazaddaruvala··on After Math
Oh dang… sorry that I fucked that up.
yazaddaruvala··on After Math
> and that mathematicians need to find out where they want to go

I think you’re right that mechanically I’m saying the same thing as they are saying “use AI to build your dreams”.

I think the psychology is the difference. Specially, “oh it can now do that too” has to be met with “finally” rather than “no way! That was supposed to be human only”.

eg “what are we after?” Is also likely a question that will be solved by AI in N years after mathematicians chip at it for all that time.

Any and every singular focus will be eliminated. There will be more tho to work on - that’s where the purpose rebirth is. I think.

Maybe said differently, I think one day these same authors will write the post - “more of math is handled by AI. It doesn’t matter. We will work on the infinite amount of it that’s left. Whatever that happens to be, even when we are surprised it wasn’t what we tried to control it to be.”

That will be acceptance. That we’ll be purpose rebirth.

yazaddaruvala··on After Math
I think you’re likely right about the path to enlightenment. I love the wisdom you’ve found. The rest of us need some time to get there, in a likely rolling wave of realization that keeps getting reset across generations.
yazaddaruvala··on After Math
Look, I could be wrong. That said, I think AI is both in some conversations a tool and in some conversations it’s short hand for “Capitalistic Acceleration”. With each iteration of RSI, this second context is increasingly the more important mental model.

Maybe reread my comments in both contexts.

Capitalistic acceleration will most definitely keep trampling on anything in front of it. Because, the humans with capital will steer it that way.

Eg OpenAI steering the “AI the tool” at Navier Stokes on a rumor (inaccurate as we found out) of Anthropic having solved it.

yazaddaruvala··on After Math
You might also be going though purpose death which is an emotional concern related to thriving, but I think your bigger emotional concern is related to survival. This answer is the same as ever - race to financial freedom. Live under your means. Invest wisely. Survive till you hit your milestones.

Meanwhile, I really don’t believe the narrative about fewer jobs.

As long as you’re curious, as long as you continue learning, the new tools and focus on the parts of your current job that involve judgment you will continue putting food on your table as long as you are alive.

Use any and every tool you have to save the people around you time, and the C level will continually fight to keep you.

When AI gets good at something you are good at - great use the time (accelerated by using AI for self help) to find another thing you’re good at the AI isn’t yet. Make sure you have 3-4 things you’re good at at any given time so as AI gets good you have redundancy.

yazaddaruvala··on After Math
I’m glad you found something that works well for you. For me, nihilism is much like ice cream: I don’t want it in my fridge - not because I think it’ll taste bad, but because I think it’s gonna taste real good.
yazaddaruvala··on After Math
Thanks for the German word. I can’t read most of the literature, but initial glance it does indeed seem the same.

FWIW I never enjoy naming things lol. I agree death and temporary seem at odds. “Purpose Loss” didn’t have the same gusto. I mostly riffed the vocabulary and definition off “Ego Death” https://en.wikipedia.org/wiki/Ego_death

yazaddaruvala··on After Math
I think as a civilization we need to postulate a new term: “purpose death”

Defined something like: temporary state of complete loss of personal purpose and the experience of existential dread from never achieving self-actualization in spite of the tremendous time commitment towards excellence in a now automated intelligence.

I truly think because of the pace of innovation this will be a universal feeling for every human for the rest of existence.

As a software engineer, I myself have only recently recovered from it. So, it’s really interesting to watch a prominent figure in their industry publicly go through “purpose death” and the related grief. It’ll be a useful case study to re-read his written meditations through this cycle.

I’d say Terrance has recently left the denial phase, the anger phase I’m sure he wisely kept off the Internet, and is currently in the bargaining phase - ie scrambling to change the goal posts. I wonder if he will wisely keep the depression / burnout phases also off the internet.

However, soon as the goalposts keep falling, I think like most humans he will accept, retool, and come out of this grief with renewed purpose with larger expectations of himself and mathematics. This recent post even starts towards some of that - but sadly is slightly off the mark.

“The important question is, therefore, not whether AI will defeat mathematicians, but which mathematical ends we want AI to serve.”

He still thinks there is controlling AI. AI will run and trample anything that stays in front of it. He needs to one day find acceptance in letting AI run while he learns how to suggest it minor course corrections which it may or may not accept, and when it doesn’t accept quickly learn from the AI why he was right or wrong.

I maybe wrong, but I think this is the cycle of “purpose death” we will all have to contend with in our own time.

yazaddaruvala··on Animation in Bevy: The Big Picture
Anyone with familiarity know when an engine like Bevy will have (or already has) plugins for simulated movement animation?

In my most recent experimental game I’d like to be able to just assign BiPed / QuadPed to the asset mesh + rig and let the engine handle the rest. Ideally, allowing me to build custom animations for attacks (or even custom movement animation like a limp) and have those blend into each other and also blend into / outof the default movement animations.

Inspired by https://youtu.be/FM8yNkWad1w?is=XV3FmLG4IPvTWknh

yazaddaruvala··on Asus Bike Booster
Ouch, love to see a great product like this. However, hate to see that bike theft wasn’t discussed at all.

“Easy installation” with two screws seems like a benefit to customers except when they come back to their parked bike only to find their expensive mod also had a hidden feature: “easy uninstallation”.

yazaddaruvala··on Ten advances in mathematics and theoretical computer science
Predicting when the sigmoid bends is difficult and predicting how long until it unbends is equally difficult.

The simpler assumption is that over enough time, the S functions stack together for long enough that working backwards from exponential is a better predictor of reality.

These stacked S curves have continually been true with most technology.

yazaddaruvala··on A full body MRI earns you a year of smoking
The title and intro are badly worded.

The conclusion is “you should do MRIs it is equivalently beneficial as all of ___ are bad for you”

yazaddaruvala··on New research suggests people can communicate and practice skills while dreaming
I think the Rick and Morty episode mathematically proved the futility in trying such an exercise.
yazaddaruvala··on CPUs Aren't Dead. Gemma2B Out Scored GPT-3.5 Turbo on Test That Made It Famous
I’ve been using Google AI Edge Gallery on my M1 MacBook with Gemma4B with very good results for random python scripts.

Unfortunately still need to copy paste the code into a file+terminal command. Which is annoying but works.

yazaddaruvala··on Supply chain nightmare: How Rust will be attacked and what we can do to mitigate
An extremely verbose effects system can resolve these dependency permissions at compile time.

However, balancing ergonomics is a the big challenge.

I personally would prefer less ergonomics for more security, but that’s likely not a broadly shared opinion.

yazaddaruvala··on Data centers in space makes no sense
I’m surprised everyone is worried about heat dissipation.

Datacenters in space is ambiguous enough to mean on lunar soil which provides plenty of heat dissipation using geothermal heat pumps.

Similarly mass to orbit is also less problematic if silicon factories (including the refineries) are built on lunar soil as well.

yazaddaruvala··on Rust--: Rust without the borrow checker
Of course it is. C does allow named functions and variables. C doesn’t allow arbitrary jumps.

Those are two reasons why C is less tedious than assembly.

yazaddaruvala··on Sora, AI Bicycles, and Meta Disruption
It does not. The $1 of electricity can be simplified to just a $1

However, the way the parent worded it ie $1 of compute electricity - requires the compute to exist and temporarily be loaned. Otherwise “just a $1” would require a massive capex to buy/build compute.

yazaddaruvala··on Failing to Understand the Exponential, Again
Self driving cars have existed for at least a year now. It only took a decade of “1 years away” but it exists now, and will likely require another decade of scaling up the hardware.

I think AGI is going to follow a similar trend. A decade of being “1 years away”. Meanwhile, unlike self driving the industry is preemptively solving the scaling up of hardware concurrently.

yazaddaruvala··on Apple's Claimed Private Data Flows Pass Through Amazon Infrastructure
Having both worked at Amazon and still in the cloud industry, to me this seems like a strange take.

Apple leases these computers from Amazon like it would from any other colo. Why wouldn’t these servers be considered Apple servers?

Barring a major privacy violation by AWS (which doesn’t seem likely), or some other sort of 0-day hack the data on these servers is entirely private to Apple.

Page 1 of 34Next →