sestep
Re:LLMs are making formal software verification feasible at a much lar...
on Friday October 23, 2026 @08:12AM (#50207731)
Yeah. I've been considering asking my boss about open-sourcing it but I'm probably gonna flesh it out a lot more first.
Re:LLMs are making formal software verification feasible at a much lar...
on Thursday October 22, 2026 @10:12PM (#50203721)
No existing semantics are enough for my goals, so I'm building my own based on Vellvm, and proving "equivalence" theorems to it and other related work that specify what quirks/discrepancies/idiosyncrasies they have with respect to each other.
Re:LLMs are making formal software verification feasible at a much lar...
on Thursday October 22, 2026 @09:40PM (#50203534)
Yeah it took a bit to decide which abstraction level to target but I ended up choosing LLVM IR (planning to try PTX soon). It's been pretty successful so far for SIMD stuff, although proving theorems about concurrent programs seems a lot slower so far.
Re:LLMs are making formal software verification feasible at a much lar...
on Thursday October 22, 2026 @09:39PM (#50203523)
My Rocq setup directly reads my actual code. And I fuzz my semantic models against the real machine.
Re:LLMs are making formal software verification feasible at a much lar...
on Thursday October 22, 2026 @08:56PM (#50203196)
Been doing this at work for the past couple weeks. Extremely powerful to be able to have an agent open a PR with some experiments showing it makes some function faster using SIMD or CUDA, and just confidently merge it because the PR has a Rocq proof that it's behaviorally equivalent to the original implementation.
Re:An Update on Orion for Linux and Windows
on Saturday October 03, 2026 @04:21PM (#49947425)
But it's not browser diversity in the sense people usually mean when they talk about IE and Chrome. It uses the same WebKit engine Safari uses.
Re:An Update on Orion for Linux and Windows
on Saturday October 03, 2026 @08:02AM (#49943527)
For me the answer is quite simple: it's the only browser on iOS that lets you run Chrome extensions and Firefox add-ons.
Re:Satin: Dark mode PDF reader via affine mapping on Oklab lightness d...
on Monday September 28, 2026 @05:15PM (#49884464)
Currently I remap all backgrounds, text, and vector graphics, and I leave raster images alone. This works great for documents whose only raster images are photographs; some documents do have other raster images that might even have white backgrounds instead of transparent, so that's not ideal, but it seems to work decently well in practice.
Re:Silicon Valley sees AI as the solution – for everyone else
on Wednesday August 05, 2026 @10:20AM (#49183350)
Full title: "Silicon Valley sees AI as the solution – for everyone else, it’s the problem"
Re:Better Models: Worse Tools
on Saturday July 04, 2026 @05:59PM (#48789473)
> In case you are curious about Fable: I intentionally did not test it because I was not sure if the classifiers they are running might downgrade me to Opus silently.
Is this still a thing? I thought Anthropic walked back the silent downgrades so now all the different domains downgrade non-silently.
Re:AI Is Designing Radio Chips That Humans Couldn't Even Imagine
on Saturday June 27, 2026 @07:20PM (#48702771)
> The famous E=mc^2 it's just the first term of a Taylor expansion.
Is this actually true? My understanding was that E=mc^2 is exact for a particle at rest.
Re:Ported my C game to WASM, here's everybug that I hit
on Monday June 15, 2026 @08:07AM (#48540113)
It's slower. Wasm32 can just reserve 4 GiB of the virtual address space from the OS for each memory, so checking for out-of-bounds memory accesses imposes no performance penalty. Wasm64 can't do that, so each memory access is a bit slower.
Re:Shall we play a game? – LLMs use tactical nukes in 95% of simulations
on Thursday June 11, 2026 @05:19PM (#48496563)
This is just false. The article links to the 46-page paper [1] which lists full prompts in section E.2.
Re:Elixir v1.20 released: now a gradually typed language
on Wednesday June 03, 2026 @03:21PM (#48388593)
I've seen various posts about Elixir's gradual type system pop up on HN, but haven't been following too closely. Does anyone know whether this particular gradual type system can change the asymptotics of programs vs untyped code? As far as I'm aware, most gradual type systems (e.g. Racket) can make programs run asymptotically slower, although there are some exceptions [1].
Re:Stop Advertising in Your Commits
on Tuesday May 26, 2026 @03:41PM (#48284944)
For sure, and in the PR description for the Nixpkgs AI policy, they explicitly mentioned this as a "brown M&M test" [1]. I read the blog post as being against including this information in commit messages at all, not just about tools adding it automatically.
Re:Stop Advertising in Your Commits
on Tuesday May 26, 2026 @03:29PM (#48284779)
I mean, sure, except that many large open-source projects (e.g. Linux [1], Nixpkgs [2], etc) require this as part of their AI policy. Omit attribution in your own projects if you want, but the maintainers of these projects are owed at least that level of transparency for contributions.
[1] https://docs.kernel.org/process/coding-assistants.html
[2] https://github.com/NixOS/nixpkgs/commit/d18b8f3238abdb2cd878...
Re:Squares in Squares
on Monday May 25, 2026 @10:26PM (#48274272)
The triangular table view is fascinating. It looks like the periodic table. I wonder if there are number-theoretic lemmas (or at least conjectures?) about what "family" the optimal packing for a given number falls into (like diamond, diagonal strip, two blobs, etc). I didn't see anything when skimming the survey paper linked at the bottom of the site, but I'm sure there's a lot more literature here.
All one-byte program names in Nixpkgs
Re:A Simpler Parametrization for Modern Optimizers
on Wednesday May 06, 2026 @08:43AM (#48035564)
All I see is "Sorry, we've misplaced that URL or it's pointing to something that doesn't exist."
Re:whohas – Command-line utility for cross-distro, cross-repository pa...
on Friday May 01, 2026 @05:20PM (#47980496)
Another great tool, built on top of nix-locate, is comma. So for any program foo, if you have foo installed, you can run it like this:
foo
And if you don't have it installed, you can run it (without installing!) like this: , foo
And if multiple different packages provide a program named bin/foo then comma lets you interactively choose the one you want, and remembers your choice so you don't have to specify again unless you choose to via the -d flag.
Re:Highlights from Git 2.54
on Thursday April 23, 2026 @09:17AM (#47875419)
I agree with the other replies saying to just run the checks in CI and have the CI error message mention how to install the pre-commit hook.
I'm glad cloning a repo doesn't automatically install hooks since I strongly dislike them: I often use Git commands in the terminal but sometimes I use the VS Code UI to commit, and it's extremely frustrating when simply creating a commit runs for several seconds because of some pre-commit hook.
Re:Arch Linux Now Has a Bit-for-Bit Reproducible Docker Image
on Thursday April 23, 2026 @08:42AM (#47875054)
Are you referring to how the nixpkgs-unstable branch hasn't been updated in the past five days? Or do you have some specific software in mind? (not arguing, just curious)
Re:A Case Against Currying
on Sunday March 22, 2026 @10:25AM (#47477844)
This is an issue in Python but less so in languages like JavaScript that support "field name punning", where you pass named arguments via lightweight record construction syntax, and you don't need to duplicate a field name if it's the same as the local variable name you're using for that field's value.
Newcomb's Paradox Needs a Demon
Re:The Long Tail of LLM-Assisted Decompilation
on Monday February 16, 2026 @11:18PM (#47043668)
One of the other PhD students in my department has an NDSS 2026 paper about combining the strengths of both LLMs and traditional decompilers! https://lukedramko.github.io/files/idioms.pdf
Re:Bun v1.3.9
on Sunday February 08, 2026 @06:00PM (#46939498)
Could you clarify what you mean about Nix missing concurrency and parallelism? I often run builds using nix-output-monitor and it definitely looks like things are running in parallel, although I could be mistaken.
Re:
on Saturday January 24, 2026 @05:23PM (#46748332)
I think you can do this with Virgil, but I'm having trouble finding the exact doc page at the moment: https://github.com/titzer/virgil
Re:Ask HN: Could you share your personal website here?
on Wednesday January 14, 2026 @06:44PM (#46625708)
Re:I Hate GitHub Actions with Passion
on Wednesday January 14, 2026 @06:01PM (#46625210)
I tried this five years ago back when I was an engineer on the PyTorch project, and it didn't work well enough to be worth it. Has it improved since then?