MurphyA/hacker-news huggingface dataset:
by wizzwizz4 | 2026-02-07 18:01:29+00:00
Lean 4 is not a theoretically-interesting proof assistant. If you're interested in such things, look into Rocq (which uses CoIC, like Lean, but is more rigorous about it), the HOL logic, Isabelle/HOL's automation suite (though Isabelle proper is fairly mediocre, apart from being the thing everyone's standardised around), Lean-auto (https://arxiv.org/abs/2505.14929), and whatever SAT solvers are state-of-the-art this week. Like the tools for symbolic integration and frequentist statistics, there isn't any magic: the power comes from handling enough uninteresting special-cases that we get broad coverage. (Personally, I think there's still a lot of power being left on the table by using overly-general algorithms: sledgehammer is used to crack a lot of nuts, even when that takes quadratic time or longer.)

While CoIC has recursion "baked in", HOL does not. It turns out that we can treat structural recursion as a derived property, even over coinductively-defined types. We don't even need a notion of ordinals for this! (See https://www.tcs.ifi.lmu.de/staff/jasmin-blanchette/card.pdf and https://matryoshka-project.github.io/pubs/bindings.pdf.)

Lean 2 used HoTT, which was theoretically interesting, but not enough was known about HoTT at the time (in particular, whether it was a constructive logic – I think we have all the pieces for an explicit construction via cubical type theory now, but I don't know that anyone's put the pieces together), so that direction has been mostly abandoned. I think there's useful work to be done in that direction, but with the current state of HoTT pedagogy, I doubt I'd ever be able to keep on top of it enough to contribute; and with Lean 4 taking so much of the funding, I don't think we'll see much work in this direction until HoTT is easier to learn.

I still think you're overgeneralising. What actual thing does your poetic tree / thought / river analogy correspond to?
by cronin101 | 2026-02-07 18:02:48+00:00
This obviously depends on what you are trying to achieve but it’s worth mentioning that there are languages designed for formal proofs and static analysis against a spec, and I have suspicions we are currently underutilizing them (because historically they weren’t very fun to write, but if everything is just tokens then who cares).

And “define the spec concretely“ (and how to exploit emerging behaviors) becomes the new definition of what programming is.
by theptip | 2026-02-07 18:03:50+00:00
So is this a model baked into the VLLM layer? Or a scaffold that the agent sits in for testing?

If the former then it’s relevant to the broader discourse on LLM generality. If the latter, then it seems less relevant to chatbots and business agents.

Edit to add: this is not part of the model, it’s in a separate pillar (Simulator vs Driver). More at https://waymo.com/blog/2025/12/demonstrably-safe-ai-for-auto....
by matsemann | 2026-02-07 18:04:18+00:00
People forget or don't keep up to date on rules. Some kind of retaking the theoretical parts would at least be nice. For instance the UK has a new highway code (I've heard), and most countries it's quite different to drive now than lets say 20 years ago. For instance the amount of cyclists and the rules around that I feel drivers in Norway have a bad grasp on.

And heck, when I got my license I lived in a remote town, 3 hours away from the nearest street light. Lots of things I got away with not learning, and whatever I memorized for the theoretical test 20 years ago is mostly forgotten. I think many people think they "know" the rules, but really don't
by vladdoster | 2026-02-07 18:04:59+00:00
Location: Nashville, TN
Remote: true
Willing to relocate: boston || nashville
Technologies: Python, Django, IaC, Terraform, Golang, CI/CD, Azure/AWS, {ba,z}sh, Lua, Springboot,
Redis, Docker, Open Service Broker, {,non}relational & vector dbs, shared services, SOA
Email: mvdoster@gmail.com

resume: https://linkedin.vdoster.com && http://github.com/vladdoster

sr. cloud software engineer @ Mastercard (5 years)

Designed and built Platform-as-a-Service for microservice workloads running on Azure and AWS
to migrate on-prem workloads to the cloud. The platform operates globally, allowing teams to
deploy to several Azure-backed regions worldwide. Helped plan and create regional landing zones
in Azure for application teams wanting to perform globally. Designed platform components using
Terraform, Go, and Node; developed support tooling using Bash, Python, and Azure CLI. De-risk the
platform by addressing security vulnerabilities and ensuring the platform is PCI compliant.

api/devops software engineer @ Harvard Medical School (2 years)

Worked as part of the DevOps team to manage a 15k core CentOS HPC cluster. Designed and implemented
Python-based security scanning pipeline to securely deploy & run Apptainer images via SLURM.
Coordinated cross-team emergency patching eﬀorts. Collaborated with researchers and engineers across
3-letter institutions to deliver secure research infrastructure. Built CI/CD Pipelines with GitHub, Jenkins,
to automate code builds, testing, and deployments. Wrote Puppet modules to manage configuration of HPC fleet.
Wrote custom Puppet module & Python scripts to automatically remediate Tenable findings.

full-stack software engineer @ Global Prior Art (3 years)

Used Django, Celery, Selenium grid, and AWS API Gateway for IP rotation to scrape USPTO patent PDFs,
apply CV for data extraction, and generate reports with relevant claims, saving employees 4-5 hours daily.
Wrote E2E black-box/fuzzing unit tests. Automated on-premise deployment via Github Actions and Ansible.
by tenthirtyam | 2026-02-07 18:05:22+00:00
My expectation is that there'll never be a single bust-up moment, no line-in-the-sand beyond which we'll be able to say "it doesn't work anymore."

Instead agent written code will get more and more complex, requiring more and more tokens (& NPU/GPU/RAM) to create/review/debug/modify, and will rapidly pass beyond any hope of a human understanding even for relatively simple projects (e.g. such as a banking app on your phone).

I wonder, however, whether the complexity will grow slower or faster than Moore's law and our collective ability to feed the AIs.
by rdtsc | 2026-02-07 18:05:35+00:00
It's his life. I can certainly look at many other lives and say they are lot of more wasted than his. Heck, he already created Mathematica, if he wanted to go and lay on the beach for the rest of this life, it would still be a lot less wasted than what many other people have accomplished in related domains.

Yeah, I don't like his arrogance, it's very grating to read. And perhaps nothing revolutionary is going to end up as a result of all the play with cellular automata but it's still interesting. Not as a rule, but sometimes discoveries in history are made by wild and wacky directions of research.
by mgkimsal | 2026-02-07 18:05:57+00:00
I read that as combined, up to this point in time. You have 20 engineers? If you haven't spent at least $20k up to this point, you've not explored or experienced enough of the ins and outs to know how best to optimize the use of these tools.

I didn't read that as you need to be spending $1k/day per engineer. That is an insane number.

EDIT: re-reading... it's ambiguous to me. But perhaps they mean per day, every day. This will only hasten the elimination of human developers, which I presume is the point.
by SilasX | 2026-02-07 18:06:11+00:00
AIUI, that's a misleading figure, because the elderly self-correct, in awareness of the greater difficulty, by driving a lot less, so the greater danger is masked in the per-unit-time accident rate.

So, in theory, policy could appropriately adjust for this dynamic by only requiring the test of over-70s driving more than X miles/year, but that adds hassle to enforcement.
by realityfactchex | 2026-02-07 18:06:59+00:00
Ribbon vs. classic toolbars is the comparison to be made. (Sorry for saying menubar when I meant toolbar up above; that was probably confusing.)

I'll try to explain the gist of it, since that seems to be the question:

As you say, one facet of ribbons is they are essentially tabs. So, ribbons obscure whatever is on "those other tabs". Often, with additional annoyance of taking more space than needed to show what they do show (which often is not want is needed). And any section within a given tab can have its own peculiar (varied) layouts. (Continuing the "find it in the hierarchy - customized for the purpose to make your life easier the way a designer thought would help!" paradigm.)

Contrast with toolbars. Show the ones you need, customize them if wanted. Icons and locations are quite effective for selecting actions. They can all be seen at once. They do what they say. No constantly interpreting the interface flow to find stuff.
by Storment33 | 2026-02-07 18:07:06+00:00
Fair enough if you've some development environment automation and you want the CI to run it as well so CI is consistent with local development.

Don't know exactly what your doing but others(myself included) are using Mise or Nix on a per project basis to automate the development environment setup and that works well on GitHub Actions.

But I don't think useradd taking 30's on GitHub Actions is a bug or something they need to fix, they've explained why. Unsure about the sudo issues, did not read it carefully.
by 3eb7988a1663 | 2026-02-07 18:07:08+00:00
Word has a billion features you did not know that exist. Getting something Word shaped is probably straight-forward enough (how long did it take to make Google Docs), but getting those dangling features and quirks would be a long haul.

Mimicking Excel - woof. This one is used by so many people in different ways, that unless you offer 1:1 bug compatibility, it would be challenging to get 100% of people to meet everyone's current use case.
by Steelclearance | 2026-02-07 18:07:10+00:00
Stoicism is an ancient (yet timeless) philosophy from the Greek and Roman era.
Basically, Stoics cultivate the basic virtues of Courage, Wisdom, Temperance and Justice, which lead to lasting happiness, success, love and all good things in life.
“The man who has virtue is in need of nothing whatever for the purpose of living well.”

Famous stoics include the philosopher Seneca and Roman emperor Marcus Aurelius
by cmrdporcupine | 2026-02-07 18:07:26+00:00
The first compiler I ever bought with my own money was a Modula-2 compiler for my Atari ST I picked up second hand for something like $100 CAD, which was a lot back in the late 80s for a teenager.

Was a mistake not to just do C, though. The Atari ST's whole OS environment was built with C void pointers and duck typing in mind.
by usefulposter | 2026-02-07 18:07:40+00:00
Selecting "Advanced" mode seems to be required in the Google Translate UI.

This is visible in all the screenshots posted to Tumblr, and per the comments there, is likely US-only at present.

Similar feature on mobile with Advanced/Fast translation models: https://9to5google.com/2025/11/02/google-translate-model-pic...

>Advanced is supported for text translation only in select languages.
by rileymichael | 2026-02-07 18:07:52+00:00
> In rule form:
- Code must not be written by humans
- Code must not be reviewed by humans

as a previous strongDM customer, i will never recommend their offering again. for a core security product, this is not the flex they think it is

also mimicking other products behavior and staying in sync is a fools task. you certainly won't be able to do it just off the API documentation. you may get close, but never perfect and you're going to experience constant breakage
by simianwords | 2026-02-07 18:07:58+00:00
I like the idea but I'm not so sure this problem can be solved generally.

As an example: imagine someone writing a data pipeline for training a machine learning model. Anyone who's done this knows that such a task involves lots data wrangling work like cleaning data, changing columns and some ad hoc stuff.

The only way to verify that things work is if the eventual model that is trained performs well.

In this case, scenario testing doesn't scale up because the feedback loop is extremely large - you have to wait until the model is trained and tested on hold out data.

Scenario testing clearly can not work on the smaller parts of the work like data wrangling.
by wouldbecouldbe | 2026-02-07 18:08:02+00:00
Yeah I completely disagree with the author actually, but also with you.

The frameworks are what make the AI write easily understandable code. I let it run nextjs with an ORM, and it almost always creates very well defined api routes, classes & data models. etter then I would do often,

I also ask it be way more correct on the validation & error handling then I would ever do. It makes mistakes, I shout at it and corrects quickly.

So the project I've been "vibe coding" have a much better codebase then I used to have on my solo projects.
by Keyframe | 2026-02-07 18:08:24+00:00
In my core I'm the same. C is my language and served me well for decades. There's nothing inherently major wrong with it until you reach one of the two (or both). Working in a group of people on a C codebase tends to introduce pain on multiple levels unlike some other languages (yes, including C++). The other is that anything takes a long-ass time to do compared to modern alternatives, which might also be an issue if you're developing a game; Especially if you're developing a game. Having said that, I can't disagree since as I said, I'm also inclined towards it's siren call of simplicity.
by data_maan | 2026-02-07 18:09:00+00:00
As mathematically interesting the 10 questions are that the paper presents, the paper is --sorry for the harsh language-- garbage from the point of view of benchmarking and ML research: Just 10 question, few descriptive statistics, no interesting points other than "can LLMs solve these uncontaminated questions", no long bench of LLMs that were evaluated.

The field of AI4Math has so many benchmarks that are well executed -- based of the related work section it seems the authors are bit familiar with AI4Math at all.

My belief is that this paper is even being discussed solely because a Fields Medalist, Martin Hairer, is on it.
by physicsguy | 2026-02-07 18:09:05+00:00
I'm not sure why this is against 'frameworks' per se; if we were sure that the code LLMs could generate was the best possible, we might as well use Assembly, no, since that'd lead to best performance? But we don't generally, we still need to validate, verify and read it. And in, that, there is still some value in using a framework since the code generated is likely, on the whole, to be shorter and simpler than that not using a framework. On top of that, because it's simpler, I've at least found that there's less scope for LLMs to go off and do something strange.
by iLoveOncall | 2026-02-07 18:10:06+00:00
That was exactly my first thought as well. All those exercises are pointless and people don't seem to understand it, it's baffling.

Even if it's not Anthropic or OpenAI paying for the solutions, maybe it'll be someone solving them "for fun" because the paper got popular and posting them online.

It's a futile exercise.
by kuboble | 2026-02-07 18:10:36+00:00
I am not in a high stakes environment and work on a one-person size projects.

But for months I have almost stopped writing actual lines of code myself.

Frequency and quality of my releases had improved.
I got very good feedback on those releases from my customer base, and the number of bugs reported is not larger than on a code written by me personally.

The only downside is that I do not know the code inside out anymore even if i read it all, it feels like a code written by co-worker.
by obirunda | 2026-02-07 18:10:58+00:00
Tokens will become significantly more expensive in the short term actually. This is not stemming from some sort of anti-AI sentiment. You have two ramps that are going to drive this. 1. Increase demand, linear growth at least but likely this is already exponential. 2. Scaling laws demand, well, more scale.

Future better models will both demand higher compute use AND higher energy. We cannot underestimate the slowness of energy production growth and also the supplies required for simply hooking things up. Some labs are commissioning their own power plants on site, but this is not a true accelerator for power grid growth limits. You're using the same supply chain to build your own power plant.

If inference cost is not dramatically reduced and models don't start meaningfully helping with innovations that make energy production faster and inference/training demand less power, the only way to control demand is to raise prices. Current inference costs, do not pay for training costs. They can probably continue to do that on funding alone, but once the demand curve hits the power production limits, only one thing can slow demand and that's raising the cost of use.
by ghaff | 2026-02-07 18:11:21+00:00
PaaS has always been this thing that isn't pure infrastructure or pure hosted software that you use as-is. Salesforce has something over 100K attendees of partners and users to its annual conference. It's always been this in-between thing with a fairly loose definition. I'd argues that Salesforce was long a cross between SaaS (for the users) and PaaS (for developers). You can probably apply the same view to a lot of other company products.
by dasil003 | 2026-02-07 18:11:21+00:00
I agree with both you and the GP. Yes, coding is being totally revolutionized by AI, and we don't really know where the ceiling will be (though I'm skeptical we'll reach true AGI any time soon), but I believe there still an essential element of understanding how computer systems work that is required to leverage AI in a sustainable way.

There is some combination of curiosity of inner workings and precision of thought that has always been essential in becoming a successful engineer. In my very first CS 101 class I remember the professor alluding to two hurdles (pointers and recursion) which a significant portion of the class would not be able to surpass and they would change majors. Throughout the subsequent decades I saw this pattern again and again with junior engineers, bootcamp grads, etc. There are some people no matter how hard they work, they can't grok abstraction and unlock a general understanding of computing possibility.

With AI you don't need to know syntax anymore, but to write the write prompts to maintain a system and (crucially) the integrity of its data over time, you still need this understanding. I'm not sure how the AI-native generation of software engineers will develop this without writing code hands-on, but I am confident they will figure it out because I believe it to be an innate, often pedantic, thirst for understanding that some people have and some don't. This is the essential quality to succeed in software both in the past and in the future. Although vibe coding lowers the barrier to entry dramatically, there is a brick wall looming just beyond the toy app/prototype phase for anyone without a technical mindset.
by CuriouslyC | 2026-02-07 18:12:03+00:00
Tests are only rigorous if the correct intent is encoded in them. Perfectly working software can be wrong if the intent was inferred incorrectly. I leverage BDD heavily, and there a lot of little details it's possible to misinterpret going from spec -> code. If the spec was sufficient to fully specify the program, it would be the program, so there's lots of room for error in the transformation.
by drcode | 2026-02-07 18:12:03+00:00
I have to stretch your analogy in weird ways to make it function within this discussion:

Imagine two people who have only sat in a chair their whole lives. Then, you have one of them learn how to drive a car, whereas the other one never leaves the chair.

The one who learned how to drive a car would then find it easier to learn how to run, compared to the person who had to continue sitting in the chair the whole time.
by rugPool | 2026-02-07 18:12:34+00:00
Back in the 00s people like you were saying "no one will put their private data in the cloud!"

"I am sick of articles about the cloud!"

"Anyone know of message boards where discussing cloud compute is banned?"

"Businesses will not trust the cloud!"

Aside from logistics of food and medicine, most economic activity is ephemeral wank.

It's memes. It's a myth. Allegory.

These systems are electrical state in machines and they can be optimized at the hardware layer.

Your Python or Ruby or whatever you ship 9,000 layers of state and abstraction above the OS running in the data center has little influence on how these systems actually function.

To borrow from poker; software engineers were being handed their hat years ago. It's already too late.
by jacquesm | 2026-02-07 18:13:05+00:00
One of my elderly uncles was in this position, but he was a bit more responsible about it than your grandfather. His way to solve it was like this: he sold his car at a discount to someone else in the same building on the condition that when he needs transport they'll drive him. It works out well, he only uses it when he absolutely has to and the rest of the time he either walks or has stuff delivered. It was a painful decision for him but in the end it worked out well (and I'm the backup driver but I'm about 100 km away from where he lives so it would always take me at least an hour to get there).
by Bender | 2026-02-07 18:13:20+00:00
How about stall this in courts until:

- Self driving vehicles are truly vs theoretically safer than humans or at least the average 70 year old.

- Self driving vehicles can be attained or reliably rented for an itsy bitsy teenie weenie fraction of a seniors monthly stipend or pension or disability. Reliably meaning no waiting line or shortages of rental self driving cars or vans.
Show HN: Semantic Search for terminal commands in the Browser (No Back end)
by jslambda | 2026-02-07 18:13:30+00:00
I wanted semantic search for TLDR pages, but also wanted it to work offline with no backend. This project runs entirely in the browser using client-side vector search:

Demo: https://jslambda.github.io/tldr-vsearch/

More information: https://jslambda.github.io/articles/semantic-tldr.html
by libraryofbabel | 2026-02-07 18:13:57+00:00
I do not really agree with the below, but the logic is probably:

1) Engineering investment at companies generally pays off in multiples of what is spent on engineering time. Say you pay 10 engineers $200k / year each and the features those 10 engineers build grow yearly revenue by $10M. That’s a 4x ROI and clearly a good deal. (Of course, this only applies up to some ceiling; not every company has enough TAM to grow as big as Amazon).

2) Giving engineers near-unlimited access to token usage means they can create even more features, in a way that still produces positive ROI per token. This is the part I disagree with most. It’s complicated. You cannot just ship infinite slop and make money. It glosses over massive complexity in how software is delivered and used.

3) Therefore (so the argument goes) you should not cap tokens and should encourage engineers to use as many as possible.

Like I said, I don’t agree with this argument. But the key thing here is step 1. Engineering time is an investment to grow revenue. If you really could get positive ROI per token in revenue growth, you should buy infinite tokens until you hit the ceiling of your business.

Of course, the real world does not work like this.
by simianwords | 2026-02-07 18:13:58+00:00
Then I disagree with you

> You still have to have a human who knows the system to validate that the thing that was built matches the intent of the spec.

You don't need a human who knows the system to validate it if you trust the LLM to do the scenario testing correctly. And from my experience, it is very trustable in these aspects.

Can you detail a scenario by which an LLM can get the scenario wrong?