MurphyA/hacker-news huggingface dataset:
by tristanj | 2025-11-27 05:33:45+00:00
You probably viewed this as a common trope because you were not aware of the actual source of the rumors. No, these are not claims are not from reddit, they're from Mark Gurman in 2018.

> Apple designers eventually hope to remove most of the external ports and buttons on the iPhone, including the charger, according to people familiar with the company’s work. During the development of the iPhone X, Apple weighed removing the wired charging system entirely. That wasn’t feasible at the time because wireless charging was still slower than traditional methods. [0]

Actual rumors include a prototype of said phone making rounds around the office.

And again, Mark Gurman from 2025:

> "But all of these changes were supposed to be just the tip of the iceberg: Apple had originally hoped to get ever more ambitious with this model... An even bigger idea was to make the Air device Apple’s first completely port-free iPhone. That would mean losing the USB-C connector and going all-in on wireless charging and syncing data with the cloud."

> "But Apple ultimately decided not to adopt a port-free design with the new iPhone, which will still have a USB-C connector. One major reason: There were concerns that removing USB-C would upset European Union regulators, who mandated the iPhone switch to USB-C and are scrutinizing the company’s business practices." [1]

[0] https://www.bloomberg.com/news/articles/2018-06-21/why-apple...

[1] https://www.bloomberg.com/news/newsletters/2025-03-16/apple-...
by parpfish | 2025-11-27 05:34:09+00:00
i hate it when the set up the half-pane in such a way that you can't adjust the water temp/pressure without being directly under the shower head.

when dealing with a new set of shower controls, i like to stand to the side and figure out what's happening and whether i need to let it warm up rather than stepping into the firing lane and taking whatever it throws at me
by zbentley | 2025-11-27 05:35:15+00:00
We have historically intervened socially (via state regulation, taboo, or censure) in areas where the likelihood of misbehavior was high or the result of misbehavior was severe enough.

For example: nuclear material possession or refinement; slavery; consumer-available systemic antibiotics; ozone-damaging coolants; dowries.

Proscriptions on those are imperfect and inconsistent worldwide, but still prevalent. Each of them is a thing which benefited many people but whose practice enabled massive harm due to human failures (like laziness).
by d--b | 2025-11-27 05:36:35+00:00
For the rest of the world: it seems way more common in the US/americas to share rooms than it is elsewhere.

Rooms with two queen-sized beds sitting next to each other are pretty standard, even in mid and high range hotels, while I’ve never seen those elsewhere.

So yeah people share these rooms as it’s usually quite cheaper than getting two rooms. I did it with friends and my in laws.
by godelski | 2025-11-27 05:36:42+00:00
I'm really annoyed by this. Not because I think Ilya is wrong, but because I think he is right. Because for years I think his current statement is right but for the same years I think his previous statement was wrong.

My stance hasn't changed, his has.

There's a big problem in that we reward those who hype, not merit. When the "era of scaling" happened there was a split. Those that claimed "Scale is all you need" and those that claimed "Scale is not enough". The former won, and I even seem to remember a bunch of people with T-shirts at NeurIPS with "scale is all you need" around that time.

So then, why are we again rewarding those same people when they change tunes? Their bet lost, sorry. I'm happy we tried scale and I'm glad we made progress, but at the same time many of us have been working outside the SIAYN paradigm and we struggled to get papers through review[0]. Scaling efforts led to lots of publications and citations, but you got far less by working outside that domain. And FFS, the reason most of you know Gary Marcus is because he was a vocal opposition to SIAYN and had enough initial clout. So as this tune is changing does the money shift towards us? Of course not.

I don't care about being vindicated, I care about trying to do research[1]. I don't care about the money, I care about trying to make AGI. Even Sutton has said that the Bitter Lesson was not about SIAYN!

So why I'm annoyed is that it seems we're going to let those who made big claims and fell short rather than those who correctly predicted the result. Why do we reward those who chase hype more than we reward those who got it right?

[0] a common criticism being "but does it work at scale?" or "needs more experiments". While these critiques/questions are legitimate they are out of place. Let us publish the small scale results first so that we can evidence our requests for more scale. Do you expect us to start at large scale first?

[1] I'm anonymous here, I don't care about the internet points. For the sake of this comment I might as well be any one of those Debbie Downers who pushed back against SIAYN and talked about the limits and how we shouldn't put all our eggs in one basket. There's thousands of us
by kragen | 2025-11-27 05:37:31+00:00
The canonical URL, dating back to at least 02015, may be http://research.microsoft.com/en-us/um/people/nick/coqasm.pd..., which now redirects to https://www.microsoft.com/en-us/research/publication/coq-wor.... This site presumably belongs to the Nick Benton who is one of its authors.
by p1mrx | 2025-11-27 05:37:33+00:00
I recently got a used QNAP TS-131P for cheap, that holds one 3.5" drive for offsite backup at a friend's house. It's compact and runs off a common 12V 3A power supply.

There is no third-party firmware available, but at least it runs Linux, so I wrote an autorun.sh script that kills 99% of the processes and phones home using ssh+rsync instead of depending on QNAP's cloud: https://github.com/pmarks-net/qnap-minlin
by mcny | 2025-11-27 05:39:00+00:00
My understanding is that the validity of the visa has nothing to do with whether you are "in status". The visa is for entry and authorized status allows you to stay in the US. You could be authorized to stay in the US and yet have to petition to get a re entry permit should you choose to leave the US temporarily.

Now I wrote this and even I am not sure if what I wrote is fully correct. I know it is correct for at least one scenario but I anal and I am sure there are scenarios where what I said is not just false but dangerously bad advice.
by serial_dev | 2025-11-27 05:39:52+00:00
> HR is to protect the company, not the employee

The CoC is not there to protect the community, but to protect all the bad actors and give ammunition to attack the good ones.

Happens every time, the maintainers who add CoCs to projects have no problem being an ahole to others.

Update: I know some people love their CoCs, but answer me this, how is this kind of childish name calling allowed and still online, if what I wrote above is not true?
by homebrewer | 2025-11-27 05:40:35+00:00
The only good thing about it is their very generous limits for "open source" projects (it doesn't even have to be free software AFAIK, just the source has to be visible to everyone).

The CI service itself is an absolute trash fire caused by the usual Microsoft NIH, and if they have financial means not to deal with it anymore, I see no reason for them to waste their limited development time on dealing with it.
by Nathanba | 2025-11-27 05:40:56+00:00
I have a lot of understanding for such personalities too, I'm probably quite like this myself although I try my hardest to not open my mouth like this. For example I got blocked by Jonathan Blow over a simple question on twitter but I don't think too badly of him now, it's just a miscalculation on his part or him trying to optimize his life as a passionate person. But you really need to make sure to be right when you are putting other people down. I mean REALLY right, you need to tripple check that what you are doing is going to help an honest person to improve themselves. So my opinion is: You can be super critical but you have to be right.

I'm not going to touch the political parts. But my main point is that the migration itself is obviously not well done, he isn't even migrating issues nor migrating perks for sponsors, splitting the community and attention apart. You could even say that he's critical of people who keep using github sponsors. In my view the text is implying that you are hurting ziglang if you keep using this thing that is a liability for ziglang... oh the horror of giving someone money in a way he doesn't like. People like this forget that contributors are doing free work for them too, it's not just one way. Everything that creates friction for them is real work you just caused them.
by quanto | 2025-11-27 05:42:53+00:00
During the days I was studying/working with Coq, one visiting professor gave a presentation on defense software design. An example presented was control logic for F-16, which the professor presumably worked on. A student asked how do you prove "correctness", i.e. operability, of a jet fighter and its control logic? I don't think the professor had a satisfying answer.

My question is the same, albeit more technically refined. How do you prove the correctness of a numerical algorithm (operating on a quantized continuum) using type-theoretic/category-theoretic tools like theorem provers like Coq? There are documented tragedies where numerical rounding error of the control logic of a missile costed lives. I have proved mathematical theorems before (Curry-Howard!) but they were mathematical object driven (e.g. sets, groups) not continuous numbers.
by kragen | 2025-11-27 05:43:02+00:00
That doesn't seem right to me. If the problem is that it has too many instructions and addressing modes, you can decide to only use a small subset of those instructions and addressing modes, which really isn't much of a handicap for implementing functionality. (It doesn't help with analyzing existing code, but neither does a powerful assembler.)

I'm no expert on assembly-language programming, but probably 90% of the assembly I write on i386, amd64, RISC-V, and ARM is about 40 instructions: ldr, mov, bl, cmp, movs, push, pop, add, b/jmp, bl/blx/call, ret, str, beq/jz, bne/jnz, bhi/ja, bge/jge, cbz, stmia, ldmia, ldmdb, add/adds, addi, sub/subs, bx, xor/eor, and, or/orr, lsls/shl, lsrs/sar/shr, test/tst, inc, dec, lea, and slt, I think. Every once in a while you need a mul or a div or something. But the other 99% of the instruction set is either for optimized vectorized inner loops or for writing operating system kernels.

I think that the reason that i386 assembly (or amd64 assembly) is error-prone is something else, something it has in common with very simple architectures and instruction sets like that of the PDP-8.
by jamesblonde | 2025-11-27 05:43:49+00:00
I have one (top of the line!). Here's how bad the engineers were. For the last 6 months, the device emits 10 audible beeps every 6 hours. I do a lot of customer meetings and public speaking. People would sometimes ask - "what is that noise"? I would say "No idea, but if you wait 8 seconds, it will stop"!

Also, my heart rate would sometimes drop below 40 bpm. Then it would start pacing, which i didn't want and was extremely uncomfortable.

p.s., the reason the battery ran out was because i found a treatment for my condition that works really well through talking globally to experts (i am a computer scientist). I wrote a case study paper about my condition to help others, co-authored by my doctors. https://www.slideshare.net/slideshow/arvc-and-flecainide-cas... 16 years later, the device is still in place, but I will have it removed early next year.
by terrywang | 2025-11-27 05:44:28+00:00
Thanks for sharing, insightful.

Personally, I consider Antigravity was a positive & ambitious launch. Initial impression was that there are many rough edges to be smoothed out. I hit many errors like 1. communicating with Gemini (Model-as-a-Service) 2. Agent execution terminated due to errors, etc., but somehow it completed the task (verification/review UX is bad).

Pricing for paid plans with AI Pro or Workspace would be key for its adoption, when Gemini 3.x and Antigravity IDE are ready for serious work.
by addaon | 2025-11-27 05:45:06+00:00
No, I haven't, but I want to. I haven't had the opportunity to go deep into formal methods for a work project yet, and on personal projects I've mostly played with Ada SPARK, not Coq. I've played with Coq a little (to the extent of re-implementing the linked paper for a subset of a different ISA), but there's definitely a learning curve. One of my personal benchmark projects is to implement a (fixed-maximum-size) MMM heap in a language, and convince myself it's both correct and of high performance; and I've yet to achieve that in any language, even SPARK, without leaning heavily on testing and hand-waving along with some amount of formal proof. I've written the code and comprehensive testing in various assembly languages (again, this is sort of my benchmark bring-up-a-new-platform-in-the-brain example), and I /think/ that for the way I think proving properties as invariants maintained across individual instructions maps pretty well to how I convince myself it's correct, but I haven't had the time, depth, or toolchain to really bottom any of this out.
by buu700 | 2025-11-27 05:45:34+00:00
I agree that that's a concern, which is why I suggested that a strict firewall around the agent machine/VM would be optimal.

Either way, if the alternative is the code not getting written at all, or having to make other significant compromises, the very edge case risk of AI randomly exfiltrating your code can be an acceptable trade in many cases. Arguably it's a lower risk than it would be with an arbitrarily chosen overseas developer/agency.

But again, I would very much like to see the tools providing this themselves, because the average user probably isn't going to do it on their own.
by petersellers | 2025-11-27 05:45:57+00:00
> To me all those mean the same thing, except the latter is more flavorful and makes my eyes less likely to glaze over.

And to many others, the difference is that one is informative, the other is likely to turn them off of the author and project forever.

I noticed that you never answered my question. If this is acceptable to you, where do you draw the line? If you can answer that question, maybe you'll be able to see the flaw in your argument.
by ryandrake | 2025-11-27 05:46:23+00:00
It wouldn’t be that big a problem if 3rd party app developers would stop dropping support for older operating systems. This is the thing that truly kills the devices.

Go to the App Store on an iPhone 7 and every app will refuse to install because it requires the latest and greatest OS even though they used to work just fine on the old OS. They deliberately drop support even when they don’t have to. Total shitty behavior.

I gotta throw away my phone because you, Mr. Developer, can’t be bothered to keep the old code around for backward compatibility.
by fireant | 2025-11-27 05:46:40+00:00
I don't think that more minutes of contact is better for anybody.

As a patient, I want to spend as little time with a doctor as possible and still receive maximally useful treatment.

As a doctor, I would want to extract maximal comp from insurance which I don't think is tied time spent with the patient, rather to a number of different treatments given.

Also please note that in most western world medical personnel is currently massively overprovisioned and so reducing their overall workload would likely lead to better result per treatment given.
by constantcrying | 2025-11-27 05:47:09+00:00
The hardware is totally ridiculous for the price. You are paying a lot of money so that the CPU can be close to your fingers, instead of in a much better cooled box half a meter away.

The OS is totally mysterious. What exactly is it? Just Fedora with a custom rice of some wm?

By the way "Entertainment, Advertising, Shopping, Attack Surface, Distraction" is something you do not have in most distros anyway. So hardly a selling point.

Who is this for? Companies with too much money? Individuals with some aesthetic sensibilities for putting your hardware right below your keyboard?
by saltcured | 2025-11-27 05:47:17+00:00
Yeah, we married in California but then left when my wife finished her Ph.D. and used up her optional practical training period on her student visa. After about four years of being an expat, I realized it wasn't for me and we started planning a return.

So, we filed the spousal petition with USCIS overseas. It was a lot of paperwork, interviews for her, and some process delays. Eventually she got her immigrant visa issued. Upon arrival in the US on that visa, it was endorsed to reflect immigration status.

This was about fifteen years ago, and as I recall the process delays were pretty much as advertised at the time. We were able to time our filing so that the visa was issued around when she would be ready to relocate.

Most of the time we spent apart was due to our conflicting career opportunities and obligations. I think the petition could have been pipelined better if I'd been willing to stick with my expat job until she also wrapped up her work there.
by holden_nelson | 2025-11-27 05:47:25+00:00
Eh I definitely agree this archetype is real but I disagree that it’s the one that constitutes the average consumer. My dad is a carpenter and my mom is a nurse. My wife is a hairstylist. None are particularly tech savvy. All three use ChatGPT quite a bit. Stuff they would previously google. How do I make an apple pie? Should I see a doctor? Stuff like that.

As another commenter stated, ChatGPT has over 700 million WAU. There are only 4.4 million SWEs in the US. I think it’s caught on
by retrac | 2025-11-27 05:48:38+00:00
No, you're right. The attack on the Death Star sequence, in Star Wars (1977), is one of the very first use of 3D computer graphics in film.

The tie-fighters and Death Star were drawn as wire-frame. And it was all wire-frame until about '81 - '82. Textured rendering was driven by rapid performance gains with parallel and vector processors. I can't think of any use of textured surfaces until the early 1980s, outside of some experimental things like "A Computer Animated Hand" (1972).

The Genesis effect in Star Trek II (1982) was considered mind-blowing at the time. Most people in the audience would have never seen anything like it: https://www.youtube.com/watch?v=Tq_sSxDE32c They used a Cray X-MP supercomputer. A very expensive one minute of film.

What we would recognize as the early 3D graphics scifi style emerges in the early-mid 80s. For example, The Last Starfighter (1984): https://youtu.be/bkDzkjQodzs?t=32
by zqy123007 | 2025-11-27 05:49:01+00:00
There are different techniques and namings. Essentially, EVERY model is biased/aligned towards something, perhaps its creator's value. China or NOT. Look at Grok and read Elon Look at Claude and Dario

I am sure OpenAI and GDM have some secret alignment sets which are not pilled towards the interet of general public, they just smart enough to NOT talking about it out loud...
by Mars008 | 2025-11-27 05:50:13+00:00
> They are born knowing how to walk

Most animals know how to walk. They have pre-build 'knowledge' and start with it when they get muscles. The main difference is some species develop muscles before they are borne. Others don't, some can't even see. But as soon as they develop they can walk without even seeing how others do it. The same way birds can learn, or be trained to fly without seeing examples. They start flapping both wings in sync, this is pre-build.
by throwaway150 | 2025-11-27 05:50:22+00:00
> the other is likely to turn them off of the author and project forever

Which is absolutely fine. It's their project, their website. If they can't be colorful on their own website, where else can they be! If it turns off some people, I'm sure the author is aware of the risk and happy with that risk.

I, for one, find this kind of colorful language refreshing. Everyone trying to be politically correct makes the internet a dull place.
Ask HN: Do teams need a tool to make IT architecture diagrams look better
by lynn_xx | 2025-11-27 05:50:42+00:00
Hi HN,

I'm exploring the idea of a SaaS that can automatically make IT architecture diagrams look professional and visually appealing.

Current tools (Draw.io, Lucidchart, Miro) are great for drawing, but diagrams often look plain, and it takes a lot of effort to make them presentation-ready.

But I am not sure if it is an actual demand. I’d love to hear from people who create architecture diagrams!
by kees99 | 2025-11-27 05:51:09+00:00
> bloated, buggy JavaScript framework

Isn't that the unfortunate status quo? At least hard requirement for JS, that is.

Google's homepage started requiring this recently. Linux kernel's git, openwrt, esp32.com, and many many others now require it too, via dreaded "Making sure you're not a bot" thing:

https://news.ycombinator.com/item?id=44962529

If anything, github is (thankfully) behind the curve here - at least some basics do work without JS.
by blahedo | 2025-11-27 05:51:45+00:00
Evidently not "clearly", given the number of people who didn't see it, but that was my first interpretation as well: I took it as an "infinite monkeys" reference that, in context, was probably standing in for "some un-tested gen AI output". Which, clicking on the link, seems to be what happened?

Anyway, yes, "infinite monkeys on typewriters" seemed to be the relevant meaning of "monkeys" here.
by jetsnoc | 2025-11-27 05:52:21+00:00
Sixteen years here, and the half-life decay of this community has been slower than anywhere else. That takes real, consistent work, and we have been lucky to have it. Through good times and rough ones, including the loss of Aaron Swartz (who I only knew of through HN), this has stayed a place for real conversation.

The grit, curiosity, and people building things have always been inspiring.

Thanks for all the discussions over the years.

Happy Thanksgiving!
by aikinai | 2025-11-27 05:52:30+00:00
Maybe I'm too stiff, but even if they don't get around to updating the laws, I'd still prefer they enforce the ones that exist so it's clear, fair, and safe. And so upstanding citizens aren't spending years separated from their spouses while they keep getting skipped by people willing to cheat the system.

It's not even a law that results in the years-long wait; it's just because the system is clogged up with other junk and understaffed. As other's have mentioned; there's no formal waiting for citizen spouses—it's supposed to be immediate—it's just that they don't even get to look at your application for years.
by dwohnitmok | 2025-11-27 05:53:20+00:00
You use floating point numbers instead of real numbers in your theorems and function definitions.

This sounds flippant, but I'm being entirely earnest. It's a significantly larger pain because floating point numbers have some messy behavior, but the essential steps remain the same. I've proved theorems about floating point numbers, not reals. Although, again, it's a huge pain, and when I can get away with it I'd prefer to prove things with real numbers and assume magically they transfer to floating point. But if the situation demands it and you have the time and energy, it's perfectly fine to use Coq/Rocq or any other theorem prover to prove things directly about floating point arithmetic.

The article itself is talking about an approach sufficiently low level that you would be proving things about floating point numbers because you would have to be since it's all assembly!

But even at a higher level you can have theorems about floating point numbers. E.g. https://flocq.gitlabpages.inria.fr/

There's nothing category theoretic or even type theoretic about the entities you are trying to prove with the theorem prover. Type theory is merely the "implementation language" of the prover. (And even if there was there's nothing tying type theory or category theory to the real numbers and not to floats)