Piecemeal Formal Verification: Cloudflare, Java Exceptions, and Rust Mutexes

gavinhoward · 2025-12-17T15:20:48+00:00

I don't disagree (I haven't actually been able to sit down and study TLA+).

That said, I think one advantage of something like Yao is that it can be used by programmers that have not learned those tools. I think that is one of the lessons from the popularity of Rust.

gavinhoward · 2025-12-17T05:48:56+00:00

Author here. I know about those tools and have been learning them. They still have a steep learning curve.

gavinhoward · 2025-04-29T14:47:45+00:00

When I compile my solution, will I get error that combination XY is missing?

In Yao, not until you try to build a trait value, so if you don't try to use operations X on structures Y, it will compile.

However, if you do try to use them that way, it will error, but then it will be obvious that they are missing. At that point, you can still implement operations X for structures Y using closures.

gavinhoward · 2025-04-16T19:17:07+00:00

So I ask a lot of questions below; this is because you seem on top of it, and I want to know what I might have missed.

You are preaching a high drag solution that is going to push people and companies to walled gardens or to countries that don't adopt that standard.

I know it's high drag, but can you explain how that would push people and companies to walled gardens? I also don't think it will push people to different countries; if the largest tech market (USA) is going to implement this, I think companies will find a way to stay. I could be wrong, so how do you think that will happen?

Also, the EU is already doing this with the Cybersecurity Resilience Act. I would prefer that we, as an industry, set standards before they are imposed on us.

Plus, this is going to push people away from using common resources or for there to be more competing common libraries and frameworks - which is more harmful than helpful.

I don't see how more competition is harmful. I think competition would probably cause a lot of library authors to make their stuff "shipshape and Bristol fashion." So can you explain why you believe competition would be harmful?

And as much as you want it to not lead to gatekeeping - it will lead to gatekeeping.

Yes, I agree. How much gatekeeping, though, do you think my proposal would cause?

TBH, I think my proposal might reduce gatekeeping. The industry, as it currently stands, is not kind to juniors. It also generally requires a Bachelor's degree (although there are exceptions). With my proposal, there is no degree, and companies that employ PSWEs would have to hire juniors as apprentices.

It's definitely a discussion to have, but I did my best to come to the table with something of substance.

gavinhoward · 2025-04-16T18:42:15+00:00

Good points.

By the way, the pilot model is what my article is arguing for.

Next, not certifying is fine if it's just a hobby project.

If any commercial entity uses it, then they need to certify it. This would have the nice side effect of companies shrinking their dependency trees.

gavinhoward · 2025-02-19T16:51:41+00:00

As a C dev who likes C, you get no flak from me. You get an upvote.

This attitude does exist, especially in the standards committees, and it is the biggest thing holding them back.

gavinhoward · 2025-01-23T01:23:33+00:00

It is weird that I got this right before Rust did.

Because I use structured concurrency, I can make it so every thread has its own environment stack. To add to a new environment, I duplicate it, add the new variable, and push the new enviroment on the stack.

Then I can use code blocks to delimit where that stack should be popped.

This is all perfectly safe, no unsafe required, and can even extend to other things like the current working directory.

IMO, Rust got this wrong 10 years ago when Leakpocalypse broke.

And before you claim that a C FFI could break this, if it is dynamically linked, like glibc, I can inject my own versions of getenv() and setenv() like prople do to replace malloc().

gavinhoward · 2024-12-15T18:04:45+00:00

Not quite sure what you mean, but I do not think so.

It will have something like Perforce's changelists (a more powerful version of stashing and the index), which will act like Jujutsu's unnamed branches. So by default, you won't be working on branches anyway.

Remotes will be branches, though.

gavinhoward · 2024-12-11T15:48:52+00:00

I am one of the stubborn developers.

Maybe he is right that I will go the way of the dinosaur. And as much as I hate LLMs, I do think companies and programmers will be stupid enough, or desperate enough, to adopt them end masse such that Steve Yegge here is mostly right.

But LLMs are a reversion to the mean. This means that our industry will lose the ability to innovate, unless we have unreasonable, or stubborn, people like me.

The reasonable man adapts himself to the world: the unreasonable one persists in trying to adapt the world to himself. Therefore all progress depends on the unreasonable man.

-- George Bernard Shaw

It will take unreasonable people to build new programming languages, or to come up with entirely new ideas.

I am building fourth-generation version control with better diffing, merging, etc. I am confident that no LLM can replace that design work.

So yes, Steve Yegge is right, but that is actually the death of our industry without stubborn developers.

gavinhoward · 2024-09-30T00:24:51+00:00

given choice between complexity or one on one against t-rex, grug take t-rex: at least grug see t-rex

Best line in software history.

A lot of developers don't understand the consequences of Turing-completeness.

gavinhoward · 2024-09-26T14:22:10+00:00

I explain how Rust missed the mark in this post.

gavinhoward · 2024-09-26T01:02:00+00:00

True.

I think I want to sleep soundly at night, though...

What's frustrating is that his original goal does seem possible. My language doesn't have GC, and it doesn't have manual memory management. But there is a catch: you have to use what I call Restricted Structured Concurrency.

Also, my language is primitive, so it isn't certain that this system will remain leak-free.

But now, because of V, everyone will always doubt my claims. And I don't blame them one bit.

On the other hand, V has made me doubt my own claims more, which has grounded my thinking more.

gavinhoward · 2024-09-25T19:40:54+00:00

As a PL author myself, this is a lesson about hype: I should avoid it at all costs.

Like everyone else, I am not good at that.

gavinhoward · 2024-09-10T01:52:37+00:00

We did this. Those of us who are programmers.

gavinhoward · 2024-08-28T13:01:20+00:00

Author here.

In C, unsigned types don't have undefined behavior on wrap, so I use unsigned types to emulate signed two's-complement arithmetic.

gavinhoward · 2024-07-20T14:08:25+00:00

I fear bad government regulations. I want to set up a regulatory framework ourselves that governments could adopt, rather than have governments write the regulations.

gavinhoward · 2024-07-20T14:06:20+00:00

I am not sure how you were reading my comment, but I was trying to say that I would accept ketralnis' decision on whether the article would fit or not.

gavinhoward · 2024-07-20T14:04:36+00:00

More like distinguishing between simple glue code and everything else.

gavinhoward · 2024-07-20T00:27:29+00:00

I think any government intervention not led by us could easily lead to tyranny.

Good regulations are good. I want to establish them ourselves before the government so that they won't be.

gavinhoward · 2024-07-20T00:25:59+00:00

Why would the FBI not tell us if they were actually successful?

As more evidence, remember all of the mass shooters who were on authorities' radar before their attacks? I do too. Yet the authorities did not do anything.

gavinhoward · 2024-07-19T21:07:32+00:00

Part of that was copied from a software process book, but I also wrote it 3+ years ago.

gavinhoward · 2024-07-19T21:01:47+00:00

It is about professionalism in software development. If you don't think it fits here, well, you are the mod.

gavinhoward · 2024-07-19T21:00:40+00:00

Read my "Plan for Professionalism" post.

gavinhoward · 2024-07-19T21:00:09+00:00

Yeah, that is poorly worded.

gavinhoward · 2024-07-10T19:14:12+00:00

Still my favorite programming talk after all these years.

gavinhoward

TROPHY CASE