davemp

> Similar to zig, odin, and others, its basically just C with some syntax conveniences.

Extremely reductive and untrue. As someone who still writes/deals with C daily, there is room for a successor that still attempts to be a thin wrapper around an abstract CPU. The C type system and preprocessor has some glaring flaws that are not fixable in a backwards compatible way.

1e1,000,000 lines of lean. Just needs human review.

DonHopkins is not a bot. Not sure about the quote though.

No they are not equal. There are a lot of hairy details usually around byte layout/endianness that are defined (sometime implementation defined) that are UB or TBDB in rust. Also rust doesn’t have int overflow UB.

Often that’s just implementation defined behavior which is perfectly safe. You should just put some compilation guards to error out if someone tries to port your code.

TCS being theoretical computer science? I have not seen that acronym before.

Have you written anything low level in Zig? If anything, Zig is lower level than C.

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

libc is even worse.

Maybe it’s wishful thinking on my behalf, but I am still not convinced that LLMs are on a path to SciFi levels of apocalyptic malicious super intelligence. Rather LLMs at some level are just all of the humanity’s information rendered accessible in an unprecedented way.

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.

AI at least with its current compute and data requirements seems structurally undemocratic to me.

Completely unrealistic. We could already be working toward such goals without super intelligent AI. I don’t see any reason to assume that ASI created through an evolutionary process would have a different outcome.

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?

I couldn’t help but notice the parent commenter’s post history. Account from literally before this was called HN, one comment 6 years later, then 13 years later this comment.

The pro lisp/s expression comments check out.

> legacy choices when we quite literally were just not smart enough to be making permanent decisions like this

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.

It should be embarrassing and shameful to apply for such a trivial patent.

> A 1963 house is what we'd think of today as a starter home.

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

Great for rich people or just not your relative purchasing power being completely eroded. Why work for a 5% raise if it means all your expenses go up 5%?

> That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use.

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.

Cool. Now we can write bugs in our theorem descriptions instead of source code.

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.

> No one is going to argue against those vague statements. He obviously does not agree with people that put more weight on making things compile errors instead of runtime errors

>> Compile errors are better than runtime crashes

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

Looks like Mr. Kelly agrees with you. From the zen of zig:

- 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.

Without explicitly entering the language holy wars. I think there’s an interesting trade-off here.

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.

I don’t think people are arguing to stop researching AGI. Moreso against sales people trying to use the concept of AGI to sell products that are very much not AGI. Or devoting so many of our resources into such a pursuit that it causes harm to real people.

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

> clueless and stubborn and confidently wrong

Uhuh. I really shouldn’t be replying to this type of comment from a throwaway.

But the extremely powerful semantic search that we get from LLMs isn’t enough. I don’t think anyone is credibly arguing otherwise?

Agents already are a layer on top trying to bridge the gap. But they’re really just using LLMs as a heuristic to explore extremely NP problem spaces. The notable successes with agents so far are when we can provide them with a solid verifier and preferably additional context hints on the steps to take in the problem space. See the test oracle problem on where this gets us.

So forgive me if I think that it would be enough of a jump in computational complexity to remove those guard rails that it’s not feasible. But don’t say that I’m clueless, stubborn, or confidently wrong.

There is a vast gulf between theoretically possible and technologically feasible.

If you can’t provide a realistic path to achieve something, you’re asking people to believe in science fiction.

You could tell me that a rock’s molecules are comprised of protons, neutrons, and electrons. Blood is also entirely protons, neutrons, and electrons; so theoretically, one could rearrange stone into blood. But without an actual method to do so, it sounds like you’re telling me that you can squeeze blood from a stone.

> the human brain exists, it is not made of magic, it can reproduced

Yeah. It only takes 9 months and ~18 years of training…

> But saying that the human brain cognitive capabilities cannot be reproduced on other types of substrates is stupid at this point

Let’s be clear. Everyone is talking about silicon transistors here. That’s what we’ve got.

Digital computers have real limits. Sensors and other sources of training data have real limitations. It’s not clear that we can organize them in a way to reproduce organic brains.

Totally insane that they enshrine this stuff in law without a reference design and corresponding data to validate its effectiveness.

Yeah I think that’s the difference. On the east coast in July, the big safety risk with fireworks is generally to your own person.

EDA tools have been using ML techniques for >10yrs afaik

It definitely isn’t simple, but it’s a pretty well trod path. If the FCC or state equivalent doesn’t have folks who can write the spec that’s a huge problem. I would be surprised if an existing spec doesn’t already exist that just needs to be applied to this scenario.

The streamers should be responsible for the signal. If the device front end has crazy frequency response or the backend does weird DSP tricks, that’s on the device manufacturers.

Article reeks of LLM mannerisms in a pretty obnoxious way. I read it anyways and surprise surprise, it boils down to:

- Ridiculously NP problem space that we guess and check with ML heuristics.

- Problem: not enough training data

Cool enough work, but the LLM generated fluff in the article really takes away from it.

Picking up on some dunning kruger effect here.

Programming isn’t even a field in the same way as prob&stats. Computer science does in fact have non-deterministic sub fields such as information theory.

Just because it could be worse doesn’t mean it couldn’t be better.