Hacker News: Jhsto

New comment by Jhsto in "Code-execution flaw in UEFI firmware threatens most servers on planet Earth"

Jhsto — Wed, 28 Oct 2026 03:22:09 +0000

Suppose the server only boots signed images created by itself, which the PXE server happens to serve. You cannot just switch or mess with the menu. But if you can exploit the boot chain before any Secure Boot components run, then you might find your way in.

New comment by Jhsto in "UK to charge universities $1,200 per international student"

Jhsto — Tue, 27 Oct 2026 07:23:03 +0000

After Brexit the tuition even for Europeans increased from 10K£ pounds a year to 40K£. A thousand pounds will not change much. It does of course change the kind of people they can admit from abroad, but it seems that the UK has a lot of demand. When I did an Erasmus MSc funded by the EU, I was the only European in the whole cohort. Many peers explicitly told me that they applied to get a chance to stay in Europe after they graduated. Most did.

New comment by Jhsto in "Sony Retires Its Last 4K Blu-ray Player in Japan, PS5 Is All That's Left"

Jhsto — Fri, 23 Oct 2026 22:21:58 +0000

Some of my friends insist on watching movies only in 4K, but once I secrectly played a proper 1080p BluRay copy and they would not believe it was 1080p.

Not much to do with the OP other than that it's been a long time since even the "tech-savy" have watched anything on disc. I guess 95% or more live with whatever potato bitrate they get from streaming services.

New comment by Jhsto in "Plex laid off the whole player team"

Jhsto — Wed, 21 Oct 2026 21:21:40 +0000

Remember that there are alternative playback clients which use Plex's backend. Infuse is one, but I think VLC also works. Both have Apple TV apps.

New comment by Jhsto in "People hooked on vapes try a new way to quit: cigarettes"

Jhsto — Wed, 23 Sep 2026 08:23:01 +0000

Anecdotally, this does work -- whenever I have had a break from nicotine pouches, I have done with cigarettes. The big difference is that with cigarettes you have to excuse yourself to go outside. It's much easier to break the habit this way. Though that might be in part how with nicotine pouches the act is different as well. Note that the nicotine content does go down this way -- I would say that the specific brand of cigarettes I roll are around 8mg in "Zyn" equivalent, which are usually sold in varying strengths from 3 to 12mg. Snus is a similar product sold usually at 8 to 24mg, though specific brands at 48mg exist.

The real challenge is that the difference between one cigarette a day and zero is huge, at least for me. Once you are at one cigarette a day, and e.g. commit to it being after a workday, you start waiting for the end of workday. It's easy to start feeling that the day does not begin until that moment. Real withdrawal starts at around day 3 and takes roughly 21 days for me.

I think smoking cessation products like patches and gum is not really helping either. It's still nicotine. I have wanted to try Varenicline, but it requires a doctor's prescription and (seemingly) "strong enough" dependence. I have hated the idea of paying 100 euros for a doctor's appointment to maybe get a prescription that costs me another 100 euros.

I plan to quit nicotine for good next month, when I submit a dissertation. After roughly 7 years of using snus and nicotine pouches, I have noticed that my gums are retracting, and when I eat food, a lot of it gets stuck at my lower teeth, and there are gaps between my teeth. I would not be surprised if I need braces, and in part wish that would solve the problem -- the gum retraction itself is irrecoverable. I have been waiting for a doctor's appointment to have my teeth checked out for about 6 months now. I can't help but think that in the process of doing my dissertation, I have trashed my health, at least to an extent, and now I'm just waiting to get an assessment how badly. Moving on, I think that whatever I'm about to do next, it should be something that I feel like needs no nicotine for motivation.

New comment by Jhsto in "ReBarUEFI: Resizable BAR for almost any UEFI system"

Jhsto — Wed, 23 Sep 2026 07:47:00 +0000

You most likely have this enabled and unless you run some ancient board. This UEFI mod is for motherboards from circa 2018. For workstation machines that would be 1st and 2nd generation Threadripper. So, if your CPU's model name starts with 3 or higher (and you have an AMD workstation), you likely have this already enabled by default.

New comment by Jhsto in "Copying login keychains between Macs fails on Secure Enclave Macs with Tahoe"

Jhsto — Fri, 11 Sep 2026 20:07:52 +0000

Switching from macOS to Linux was quite painful because the security was so seamless on Mac. But I also realized I had no idea how my passwords are stored and under what guarantees. Learning and getting the hardware tokens to do it properly on Linux was a PITA. But reading this post made me feel a pinch better.

CUDA Rust: Two Tracks for Writing GPU Kernels

Jhsto — Wed, 09 Sep 2026 13:18:33 +0000

Article URL: https://developer.nvidia.com/blog/introducing-cuda-rust-two-tracks-for-writing-gpu-kernels/

Comments URL: https://news.ycombinator.com/item?id=49626073

Points: 5

# Comments: 0

New comment by Jhsto in "Fermat's Last Theorem in Lean 4"

Jhsto — Sun, 06 Sep 2026 09:40:02 +0000

It indeed does, this is a very good point I haven't thought about in the reverse direction.

South Korea exports surpass full-year record, hit $709.4B YTD

Jhsto — Sun, 06 Sep 2026 09:37:48 +0000

Article URL: https://www.reuters.com/world/asia-pacific/south-korea-exports-surpass-full-year-record-hit-7094-billion-ytd-2026-09-05/

Comments URL: https://news.ycombinator.com/item?id=49584772

Points: 3

# Comments: 0

New comment by Jhsto in "Fermat's Last Theorem in Lean 4"

Jhsto — Fri, 04 Sep 2026 21:54:04 +0000

My anecdotal experience is that while LLMs are quite good at closing theorems given an LSP to inspect the proof-tree, they suffer from similar kind of problems with proofs as they do with bigger codebases in any language -- finding reusable parts that can be built into libraries (that's lemmas in Lean 4 sense). However, Buzzard has many times said that he wouldn't care how big the proof is and how ugly it would be, as long as there would be a proof.

New comment by Jhsto in "Rust SIMD on the GPU"

Jhsto — Tue, 11 Aug 2026 11:15:14 +0000

SPIR-V states its an int, float, vector n (where n <= 4) or a matrix (2..4 cols of vector n).

It does not necessarily mean the hardware can do 4x4x64 floating point operations in a single subgroup operation, but at least the programming model supports framing it that way.

MSI Pro B850-P WiFi Dasharo v0.9.0 Released

Jhsto — Fri, 31 Jul 2026 21:56:55 +0000

Article URL: https://blog.3mdeb.com/2026/2026-07-30-msi-pro-b850p-v090-release/

Comments URL: https://news.ycombinator.com/item?id=49129006

Points: 2

# Comments: 0

New comment by Jhsto in "Recursion is lying to you"

Jhsto — Wed, 29 Jul 2026 01:22:54 +0000

I've been writing a language around recursion schemes! Insofar it's just a library for Lean, but I wish to one day release it as an array programming language. I'm submitting a thesis in ~3 months, after which I'll be open-sourcing it.

New comment by Jhsto in "We have proof automation now"

Jhsto — Sun, 26 Jul 2026 22:19:29 +0000

As a meta-comment on the topic, something I have noticed is that there still exists confusion what it means to use theorem provers for projects -- the other day I read a tweet from Paradigm, a crypto-VC now seemingly AI-pilled. Some LP of theirs had made a Lean 4 formalization of the Ethereum's virtual machine. The tweet said this would have cost like $150k in API tokens ("would have", as in, I guess they get theirs for free), and took a week of inference time for an LLM to produce. I somehow got distracted to actually take a look at the code, which I found rather light on theorems. Nor did the project make use of Batteries or Mathlib which are arguably the one of the strongest motivation for me personally to use Lean4. That is, I generally rather rely on someone else getting the category theory and algebraic structures right, which then leaves me the proof obligation to show the correspondence with whatever toy I'm working on. Here I'm fine to use LLMs for proof search, very similar to how would I use a SMT solver. But what I have found is that the language models have to be really coerced into using these libraries, because otherwise the models much rather overfit and overclaim a solution with a 3 minute inference task rather than attempt to fulfill the proof obligations over 3 hours. And I feel nauseated when I need to convince the LLM (I use Claude) that filling the proof obligation is for "academic exercise" or because I'm coerced into doing so, because otherwise it will come up with reasons of its own why it does not want to do it. Now, this happens under the mental model in which I'm interested in finding equivalences with prior work. Many LLM generated Lean code reads more as if someone was interested whether X can be turned into a Lean 4 program, which is mostly yes, and that in general is a positive thing. But, if you are not interested in refinement types and theorems, why not just choose Haskell? The point is, I strongly sense that unless you have good questions to ask, then that's very evident in these languages. And, this is something the LLM won't help you -- if you don't impose a proof obligation for it, it certainly will not try to go the extra mile to conjure one for you.

New comment by Jhsto in "Vulkan Tutorial"

Jhsto — Thu, 23 Jul 2026 20:59:59 +0000

Another good tutorial: https://hoj-senna.github.io/ashen-aetna/

I used that to create my own Vulkan compute loader https://github.com/rivi-lang/rivi-loader

New comment by Jhsto in "Train sim created by just one person is being called the best ever made"

Jhsto — Thu, 09 Jul 2026 22:36:32 +0000

Anecdote, but I recall my friend saying he worked on freelancing assets to some train game and showed me some pictures of the said game. Unless there are more of these in existence, I think it was this.

GeForce Trading Cards: Series 1 Celebrates the Generations of GeForce

Jhsto — Thu, 09 Jul 2026 22:27:04 +0000

Article URL: https://www.nvidia.com/en-us/geforce/news/geforce-trading-cards-series-1-summer-of-rtx-giveaways/

Comments URL: https://news.ycombinator.com/item?id=48853206

Points: 1

# Comments: 0

New comment by Jhsto in "I Changed My Name"

Jhsto — Thu, 09 Jul 2026 22:18:12 +0000

I have this weird thing about a birthday -- for some reason, I was assigned a different birth date in NHS records in the UK compared to the one I have in my native Finland. I want to believe it has something to do with electronic systems transacting with different countries' systems (I noticed this difference soon after I exchanged my driver license) -- and I would have indeed born on a different day if it'd been the UK. But, I would assume this to be such a well-known issue with people who migrate, that it must just been just a typo. Doesn't stop me from believing though.

New comment by Jhsto in "Applied Category Theory Course (2018)"

Jhsto — Sat, 04 Jul 2026 10:59:09 +0000

Kiitos! My level is graduate, but part of the challenge with category theory is that some of the terms are quite unsuggestive. I feel that after seeing enough examples, I can start making more sense what some concept would be in Finnish, which helps me remember what was what and what it might relate to.

Edit: Also realized you're in Oulu, feel free to email me if you'd be up to meeting in-person to discuss these further!