Hacker News: smasher164

New comment by smasher164 in "Introduction to Formal Verification with Lean Part 1"

smasher164 — Wed, 22 Jul 2026 13:17:13 +0000

a) Thanks for putting this together!

b) Please don't hijack my scrolling.

c) I really wish Lean were more mature as an application programming language. Its standard library is really lacking.

New comment by smasher164 in "Ask HN: Did Fable disappear from your Claude usage and requires credits now?"

smasher164 — Fri, 17 Jul 2026 18:29:04 +0000

They might use this bug as a reason to be able to extend it for another week or something.

New comment by smasher164 in "Rewriting Bun in Rust"

smasher164 — Thu, 09 Jul 2026 03:22:54 +0000

It's still shocking to me that the approach taken wasn't to have Claude write a tool that translates Zig to Rust. I imagine it would've been cheaper, deterministic, and each iteration would produce a better tool.

Flint: Fast Library for Number Theory

smasher164 — Mon, 29 Jun 2026 18:34:21 +0000

Article URL: https://flintlib.org/

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

Points: 11

# Comments: 0

Type Inference (Part 1)

smasher164 — Fri, 26 Jun 2026 20:58:36 +0000

Article URL: https://www.blog.akhil.cc/type-inference-part-1

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

Points: 2

# Comments: 0

New comment by smasher164 in "Running Windows Games on a Hobby OS with Wine"

smasher164 — Wed, 24 Jun 2026 17:51:00 +0000

If you have a goal of making your OS usable, you have to design it with this in mind. Build your kernel and driver subsystem in a way that legacy OS interfaces can be implemented on top of them. Find ways to repurpose existing infrastructure so you don't have to do all the work yourself.

New comment by smasher164 in "Show HN: Microcrad – Micrograd Reimplemented in C"

smasher164 — Sat, 20 Jun 2026 18:07:01 +0000

I guess I interpreted this part of their README as implying that the author found RC too fragile

> Reference counting buys correctness and composability, but at a cost.

> Disadvantage #1: you must balance every reference. Each value_create, value_retain, and each operation's implicit retain of its operands has to be matched by a value_release. Forget one and you leak; do one too many and you free memory that is still in use. The training examples in examples/ are verbose precisely because they are scrupulous about this in their error paths; that verbosity is the price of leak-free C.

New comment by smasher164 in "Show HN: Microcrad – Micrograd Reimplemented in C"

smasher164 — Sat, 20 Jun 2026 17:28:13 +0000

Is there a reason you didn't go with something like Boehm for a library gc, instead of writing your reference counting implementation?

New comment by smasher164 in "LLMs Are Complicated Now"

smasher164 — Sat, 20 Jun 2026 17:25:19 +0000

lol yeah I guess the best move right now is to fetch their /feed and iterate through s

New comment by smasher164 in "Cargo-Geiger"

smasher164 — Sat, 20 Jun 2026 17:20:21 +0000

I think what would matter from this kind of measure is whether a project's use of unsafe actually has undefined behavior. Like the number of unsafe blocks is not really my concern as much as what the unsafe blocks are doing. If you build a single faulty abstraction via unsafe, anything that uses it is broken.

In my projects, it usually comes down to a scenario like needing to write inline assembly or invoke a foreign function, where there are close to zero guarantees the language can give me.

Portsh: A batch/shell polyglot that implements a Lisp

smasher164 — Tue, 16 Jun 2026 22:53:43 +0000

Article URL: https://github.com/smasher164/portsh

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

Points: 31

# Comments: 0

New comment by smasher164 in "Feds freaked over Fable 5 after 'fix this code', not jailbreak, say researchers"

smasher164 — Tue, 16 Jun 2026 17:02:27 +0000

Honestly, given how trivial it is for mythos-class models to identify an exploit, I’m going to assume any sufficiently large project written in C, C++, or Zig is riddled with latent vulnerabilities and compromised.

New comment by smasher164 in "Formal methods and the future of programming"

smasher164 — Mon, 15 Jun 2026 01:50:58 +0000

I think it's a good time to learn Lean. It positions itself as a proof assistant that's also good at practical programming. I'm not sure how mature the ecosystem is for the latter.

New comment by smasher164 in "Restartable Sequences"

smasher164 — Mon, 01 Jun 2026 02:18:27 +0000

I was having a conversation with someone recently if RSEQ would be a good primitive to build a load-link/store-conditional implementation in user-space. It gives you a critical window, though you still have to deal with spurious restarts, and provide a way for one core to abort another.

New comment by smasher164 in "Perry Compiles TypeScript directly to executables using SWC and LLVM"

smasher164 — Sat, 30 May 2026 17:41:24 +0000

On other sites, like github and reddit. This exchange was funny though. He eventually gets called out by the other commenter to stop responding with an LLM: https://github.com/PerryTS/perry/issues/139#issuecomment-429...

New comment by smasher164 in "Perry Compiles TypeScript directly to executables using SWC and LLVM"

smasher164 — Sat, 30 May 2026 05:09:12 +0000

I'm not against AI usage but the website, documentation, and even the comments the creator (proggeramlug) makes in response to questions are all very clearly AI-generated. Also, as someone else noticed, the pacing of the commits is eerily fast. That combined with the level of functionality makes me dubious how much accountability the creators have over the implementation.

Like you really built a backend that lowers to LLVM, integrated it with a generational gc, wrote a cross-platform reactive runtime, and built support for eleven different targets within like a year? Are you just prompting the model to tack on the next coolest thing or do you understand how these features work?

I worry how many of these kinds of projects will show up now. How do you guarantee stability? If there's a memory corruption error in the GC implementation, who's going to debug it?

New comment by smasher164 in "Performance of Rust Language [pdf]"

smasher164 — Tue, 26 May 2026 06:07:44 +0000

You end up needing something like refinement types to control the way you statically enforce bounds. That being said, there's stuff like https://flux-rs.github.io/flux/ which uses macros to layer a refinement type system on top of rust's. You can use it to statically eliminate bounds checks.

New comment by smasher164 in "Making deep learning go brrrr from first principles (2022)"

smasher164 — Sat, 23 May 2026 15:52:13 +0000

> This is a category error.

Okay, but surely you know what they actually mean right, or are you being willfully obtuse? They are comparing CPython (the main python implementation)'s implementation that runs on the CPU with a kernel running on the GPU.

New comment by smasher164 in "Bun Rust rewrite: "codebase fails basic miri checks, allows for UB in safe rust""

smasher164 — Fri, 15 May 2026 18:50:36 +0000

What I don't understand is if they were going to translate Zig to unsafe Rust, why not just build a translation tool for it? You could do a one-to-one mapping of language constructs, hardcoding patterns in your codebase, and as one friend put it "Tbh they could've just hooked up zig translate-c to c2rust". They would get deterministic translation, would probably have not been a heavy investment to build, and the output would have the same assurances as the input.

In this case, I would trust the output even less than the input. The input was memory-unsafe but hand-written. The output is memory-unsafe but also vibe-coded and has had no eyeballs on it. What is the point of abusing agentic AI for this use-case?

New comment by smasher164 in "Hammerspoon"

smasher164 — Sat, 14 Mar 2026 07:06:43 +0000

One of the reasons I left macos was that automation via Automator and Applescript was inconsistent and unsupported in many contexts. Well that and the locking down of app distribution and sandboxing. However, the positive reception to Hammerspoon is making me consider trying it again.