A lot of the “high level assembly” parts of C are actually compiler extensions and not from the C spec.

libc is even worse.

In general trying to regulate information access is a losing battle that invites tyranny. So the goal should be minimal restrictions.

At the end of the day, the threats posed by capable AI tools have to be physical. I think the key threats are the following:

- Internet connected infrastructure being crippled

- Creation of WMDs

- Economic collapse (precipitous devaluation of knowledge work and IP).

I personally think the glory days of the wild west, mostly unregulated internet were already over before LLMs; and we need to take a step back to make something structurally secure. This (expensive) change would stop the irresponsible/malicious actor running a tireless hacking agent in a loop threat model. Even a rogue SciFi tier AI would have a much harder time escaping/propagating with a structurally secure internet.

Enabling WMD creation is scaring, but I don’t think it’s really that big of an issue. Anyone with a sophisticated enough supply chain to create AI data centers is leaps and bounds more advanced than what is required to enrich uranium or synthesize bio weapons. The problem is allowing access to untrusted parties. I think it’s fair enough that individual actors shouldn’t have unregulated access to all of human information (private frontier AI companies included).

The last problem is probably the trickiest, but again could probably be solved by regulation. IP protection is already tricky and I don’t think we should try to get more protectionist.

We really need to figure out how to preserve fulfilling careers (if AI does ever get cost effective enough). I don’t think, say accounting, is inherently more fulfilling than building a house. The problem is concentration of wealth and labor dynamics.

Of course all of this gets way harder if it proves that truly dangerous capabilities can be present in models that can be run on consumer hardware.

I don’t think it’s necessarily tyrannical to have a tier of hardware that’s labeled some equivalent of “weapons grade” and requires strict licensing. Restricted computers is a change from the norm. But I can go buy a shotgun with ease and not an F35 jet.

We’d just need to be careful that we can still have lightly to unregulated computing to a certain point and that access to the capable AIs isn’t restricted to just in groups.

If ASI ended up being align-able and not an evolutionary process, why would we assume folks who already are currently in power would change their behavior?

The pro lisp/s expression comments check out.

Unnecessary hubris. I assure you the original ABI authors were plenty smart and just faced a different set of problems.

> Our forebears are either not interested in a world without the mounting, crushing debt or just prefer not to tackle that mess right now

The article mentions the organizational/social part of this problem, but then goes on to drop this turd.

I can also assure you that our forebears were neither malicious or lazy; but faced the same problem this proposal does.

I don’t like seeing such disrespect for the folks who laid out the groundwork for us.

Not every house at that time was a post war levitown style shack. AC wasn’t even terribly uncommon in 1960s construction.

Really unnecessary levels of snark here.

> often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted

Have you ever heard of prolog? I’m sure a prolog program can express whatever property you’re attempting to write just as tersely (if that’s your metric for hard). Almost copy/pastable to and from a theorem proofer.

Or are you saying that the program has to be the efficient implementation? Because that’s a different ball game. I’m not even going to get into how you could provably transform brute force propositional logic into efficient algorithms. (At that point we’ll have finally created the fabled “sufficiently smart compiler” and probably solved p=np).

A huge majority of software is simple business rules + CRUD that is trivially verifiable. The entire problem is showing that an efficient/reliable program actually implements those rules.

> The magic is that you can write a spec that's clear

Maybe you can. But I did spend a grad class with rocq (coq at the time) and a decade working with “systems engineers” and am not convinced that this is a realistic expectation.

Seriously, please review Curry Howard Isomorphism if you’re getting pulled down this rabbit hole.

Programs are proofs. Proofs are programs.

So if you can formally describe the correct output for every input, you can have an LLM loop automatically fill in the gaps of how to get there. Congrats, that sounds at least as hard as writing the correct program in most cases.

Don’t get me wrong, I do think there are useful tools combining formal methods and llms. Let’s just not get carried away.

>> Compile errors are better than runtime crashes

I don’t think you’re being fair here.

- Runtime crashes are better than bugs.

- Compile errors are better than runtime crashes.

- Incremental improvements.

- Avoid local maximums.

Considering every memory safe language that I’m aware of panics on index out of bounds, there’s spectrum here.

Personally, I’d like to see refinement types that allow people to elide the runtime overhead/panics. Though that may be too much complexity to stomach.

Static analysis based approaches restrict what is possible to express in the language (See: doubly linked lists). But can have lower dynamic overhead.

Ways to work around expressiveness limitations include strategies such as using indices into an array instead of pointers. Which in turn incurs the dynamic overhead from bounds checking.

Maybe zig could find a way to elide enough of the capability overhead that careful programming could get a <2x penalty vs C. Maybe explicit opt-in built in types or something. This would essentially be the reverse of unsafe blocks, but then there’s no escape hatch.

Another key pro to capabilities is that you can actually have a memory safe interface without having to leak lifetime and other info across boundaries. This would be great for compile times and places where open source is not tenable.

Regardless, I’m very happy to see another independent school of thought approach memory safety. I’ll forgive Mr. Kelly any gruffness, these topics can be quite annoying to discuss in public.

This is obviously complicated by the fact that LLMs/Agents are useful by themselves, but that’s not really the topic at hand.