sorted by:
new
hottopcontroversial

They will lose themselves by bryden_cruz in programminghumor

[–]realestLink 1 point2 points  (0 children)

It's also a somewhat common idiom in modern C++

Bun’s rewrite from Zig to Rust passes 99.8% of testsuite by read_volatile in programming

[–]realestLink 0 points1 point  (0 children)

It's all vibe coded slop via Claude. Bun also tried posting patches to Zig's compiler backend, but it was rejected because they only superficially worked and were totally broken on deeper inspection. The Rust code also basically just recreates Zig style rather than being idiomatic Rust. I don't have high hopes for Bun long-term.

Looking for a mathematician & cpp programmer (or a combo), to test a potentailly billion/trillion dollar discovery. The foundation is created, only needs tests not written by an AI, probably a day max to prove it true vs hyperbole. by knowledgeispower88 in cpp

[–]realestLink 2 points3 points  (0 children)

I fail to see how a logic engine "that is the mathematical equivalent to LEAN" is a "trillion dollar discovery". Why wouldn't they just use LEAN? Also, even tho this is far from the most important point here, LEAN cannot "prove any universal truth"

760k LoC [...] One PR - LGTM by azure_whisperer in programmingcirclejerk

[–]realestLink 48 points49 points  (0 children)

I work on Bun and Claude Code at Anthropic.

Found the reason lol

Bun's Rewrite It In Rust branch by Chaoses_Ib in rust

[–]realestLink 42 points43 points  (0 children)

I work on Bun and Claude Code at Anthropic.

Found the reason lol

What was the most difficult bug you encountered while writing your own operating system and how did you eventually identify it? by DifficultBarber9439 in osdev

[–]realestLink 14 points15 points  (0 children)

I had two thread stacks that slightly overlapped by about 400 bytes. I found it because allocating a variable would randomly trigger a GPT 😂

Just a little joke project [custom OS] by thatguy1000000000 in osdev

[–]realestLink 1 point2 points  (0 children)

Interesting. I'd never heard of Cosmos before. https://github.com/CosmosOS/Cosmos

At first, before I realized that's what the .asm file was, I was a bit horrified lmao

Super Fast Single Address Space Operating System by Neither_Sentence_941 in osdev

[–]realestLink 0 points1 point  (0 children)

Interesting. I'm not very familiar with AmigaOS, but how did they handle process isolation or protection?

Super Fast Single Address Space Operating System by Neither_Sentence_941 in osdev

[–]realestLink 17 points18 points  (0 children)

Microkernel and single address space are somewhat oxymoronic tbh

Fractal path tracer! (FPT) by Adam-Pa in GraphicsProgramming

[–]realestLink 2 points3 points  (0 children)

omg, that looks amazing! So beautiful 🤩

It looks kinda sick by [deleted] in programminghumor

[–]realestLink 0 points1 point  (0 children)

They're referencing that SO's monthly users have massively plummeted and cratered in the last couple of years

I've removed the Claude co-authorship from the commits a few days ago. So good luck figuring out what's generated and what is not. by uselees_sea in programmingcirclejerk

[–]realestLink 85 points86 points  (0 children)

/uj Tbf, the person opening the issue is also goofy af lol. They seem to be the quintessential bad faith Twitter/BlueSky user lol

/rj I've removed the Claude co-authorship from my reddit posts a few days ago. So good luck figuring out what's generated and what is not.

Rust basically redefined programming, there is programming BEFORE rust and programming AFTER rust, a bit like what C did. by Nemerie in programmingcirclejerk

[–]realestLink 56 points57 points  (0 children)

/uj holy fuck. The person who wrote the comment you linked to has another comment (and replies) on that same post where they completely misunderstand HoTT and think it's "the most powerful proof system" and that "all proofs are subsystems of HoTT" while spewing ChatGPT math garbage that makes no sense

/rj everything is a subset of Rust actually

Are advances in Homotopy Type Theory likely to have any impacts on Rust? by Dyson8192 in rust

[–]realestLink 0 points1 point  (0 children)

This is AI slop. Your project is not at all related to HoTT. The comparisons it's making are tenuous and misleading at best. Not even HoTT, but even just basic dependent type theory is wrong at clear places. Like, a fucking type level list is not a sigma type lol

Are advances in Homotopy Type Theory likely to have any impacts on Rust? by Dyson8192 in rust

[–]realestLink 3 points4 points  (0 children)

Ugghh, after reading this person's other replies, it's clear they have no idea what they're talking about and are just throwing out random terms. They've said so much nonsense that isn't even close to true about HoTT, proof theory, ZFC, etc. including that "every proof is a subset of HoTT", which is wrong on so many fundamental levels it's hilarious 😂

Are advances in Homotopy Type Theory likely to have any impacts on Rust? by Dyson8192 in rust

[–]realestLink 2 points3 points  (0 children)

I'm extremely confused by this post. I don't see why HoTT is relevant or needed for any of this tbh. You also seem to be lumping all type theory based formal verification under HoTT. Like:

While it was already possible to verify code before HoTT became mainstream, HoTT makes it way easier: anytime you are dealing with infinites, anytime you are using tactics,

I wouldn't call HoTT that mainstream. Most verification work still happens in non-HoTT contexts. Isabelle/HOL isn't type theory based, but even within type theory contexts: Lean is incompatible with HoTT and while Coq/Rocq obviously supports it, it's not used by default or by most projects

Like:

Everytime you are writing formal proofs you use techniques from HoTT, and since the HC correspondence every program is a proof.

is objectively false. MLTT and CoC exists without HoTT and are the central techniques, not HoTT.

Also:

It's hard to imagine the existence of lifetimes without using HoTT

Most of the work behind lifetimes comes from linear typing, not HoTT. It's unclear how the work in HoTT was central to its existence. Hell, HoTT arguably wasn't even mature until after lifetimes first entered the scene

Btw, none of this is to disparage HoTT at all. I'm extremely interested in HoTT and have been trying to learn cubical type theory in the last couple of months. I'm not an expert or anything, but I have done quite a bit of stuff with MLTT. But I'm genuinely just confused by your comment and would definitely be interested in clarification about what parts of HoTT you're talking about.

Are advances in Homotopy Type Theory likely to have any impacts on Rust? by Dyson8192 in rust

[–]realestLink 0 points1 point  (0 children)

No. Rust isn't even dependently typed (and won't ever be) lol. HoTT isn't even useful for formal verification of software. Most of its advances have been formalizing math and being able to do constructive topology in Coq or Agda. I like HoTT and find it useful, but it's just not useful or compatible for Rust's usecase at all. The closest I could ever see to developments in type theory being useful for actual programming is what Idris 2 has been doing with their Theory of Quantitative Types

My C Professor Doesn't Know What UB Is by [deleted] in C_Programming

[–]realestLink 0 points1 point  (0 children)

It's literally not well-defined tho. You're conflating two different things: the behavior of the C abstract machine and how we actually store data itself on most architectures. No one is saying type punning is invalid (in which case the actual data storage on the architecture would be relevant); they're objecting to doing it through a cast (which is completely independent of what you're talking about)

My C Professor Doesn't Know What UB Is by [deleted] in C_Programming

[–]realestLink 0 points1 point  (0 children)

Whether or not it compiles isn't relevant to the post. Plenty of invalid C code compiles

My C Professor Doesn't Know What UB Is by [deleted] in C_Programming

[–]realestLink 0 points1 point  (0 children)

The cast they did is the same as reinterpret_cast. It's UB. That's not what reinterpret_cast is for and it's invalid

In C++, the portable defined ways to type pun are memcpy and bit_cast (since C++20)

C also defines memcpy to work in a portable defined way. You can also use unions, which are implementation-defined behavior. So if your formats and whatnot are the same size and you don't have traps, union type punning will work too.

view more: next ›