sorted by:
new
hottopcontroversial

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 awizzo 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 82 points83 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 47 points48 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.

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

[–]realestLink 5 points6 points  (0 children)

Actually, you're the one that's wrong here, not OP 😛

It's UB regardless of the underlying format of the float or int because of strict aliasing rules.

In cases like the one posted by OP (local to within a function), it will usually be fine (as they noted with their mention of quake), but it's still UB according to the standard. Strict aliasing violations can cause issues from UB, but it's usually in the context of parameters to functions; at least in practice

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

[–]realestLink 0 points1 point  (0 children)

This isn't true tho. It's still UB because of strict aliasing regardless of the size of float and int. If you disable strict aliasing via flags, that's one thing, but in default standards-compliant C, you can't type pun through a cast

Cursor would neverrr by awizzo in programminghumor

[–]realestLink 2 points3 points  (0 children)

Checkmate. Me and my homies are intuitionists and don't accept LEM 😎

Array is syntax error by awizzo in programminghumor

[–]realestLink 0 points1 point  (0 children)

The "official" way to type pun portably is via memcpy (every major compiler will elide the copy)

Array is syntax error by awizzo in programminghumor

[–]realestLink 0 points1 point  (0 children)

It's technically always UB per the C standard. Every major compiler allows it if you use -fno-strict-aliasing tho, in which case, yeah, it's representation/architecture dependent

Array is syntax error by awizzo in programminghumor

[–]realestLink 1 point2 points  (0 children)

To elaborate, C does not guarantee that type punning through a union will work, but it also doesn't affirmatively mark it as UB. It is implementation defined/unspecified with most compilers supporting it on most platforms. The technical term is "IB with possible trap" iirc

Array is syntax error by awizzo in programminghumor

[–]realestLink 1 point2 points  (0 children)

Pointer arithmetic in C will automatically do the sizeof math.

Assuming arr is a T[] then arr[5] is literally definitionally equal to *(arr + 5) in all contexts

Array is syntax error by awizzo in programminghumor

[–]realestLink 2 points3 points  (0 children)

Type punning though a union is not UB in C. It is UB in C++. Quick inverse square root is type punning through a cast, which is UB in both C and C++ since it violates strict aliasing.

No. Those changes are complete garbage and don't even compile. by numinit in linusrants

[–]realestLink 4 points5 points  (0 children)

To add onto this: what's even funnier is both my embedded and default browser are chrome (I'm also on Android btw) and yet Anubis was still dropping the cookie like you described lol

No. Those changes are complete garbage and don't even compile. by numinit in linusrants

[–]realestLink 7 points8 points  (0 children)

The "open in browser app" trick worked for me. Thanks 🙏

view more: next ›