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.
HN user
akhil.cc
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.
They might use this bug as a reason to be able to extend it for another week or something.
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.
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.
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.
Is there a reason you didn't go with something like Boehm for a library gc, instead of writing your reference counting implementation?
lol yeah I guess the best move right now is to fetch their /feed and iterate through <post>s
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.
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.
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.
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.
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...
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?
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.
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.
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?
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.
This is very exciting! I've been longing for an acme-like editor that adapts better to mainstream OSes. Being vim-like is a major plus. I'm gonna try this out!
Does tvix support targeting windows? And I do not mean WSL. iirc, the nix attempted a windows port but there were some hardcoded assumptions made about unix in the implementation that made it intractable, for example the location of the store. Do these issues also hold for tvix?
Another approach is to use a Gc<T> smart pointer: https://docs.rs/gc/latest/gc/
I've used this in an interpreter and it's quite convenient.
these groups don't seem to be interested in fixing kernel problems
I mean, they built a whole kernel module that addresses page allocation/deallocation scalability issues. Whether that gets brought upstream, I'm not sure.
Yeah in many ways, Nix is a research project that escaped the lab. It’s the first tool of its kind that also happened to become successful. You have to write in this dynamically typed Haskell with poor affordances for being a build system and fragmented ways of addressing pinning.
I have an iphone, so I hope the serial number won’t be an issue.
Yeah, I also tend to bring up iCloud Notes in a browser tab. It’s still far from perfect, since Notes is usually an offline-first app, which you miss out on here.
I’ve been looking for a replacement, but nothing really gives you
- Offline-first usage
- Sync changes via CRDT
- Fast startup time
- Rich text support
- iOS and desktop linux support
I know this only works for cli tools right now, but I’d love to be able to run iMessage and Notes on linux.
Frink is great. If you’re looking for a more general purpose language with a units system, consider F#: https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref...
A great idea hindered by the lack of adoption in tools.
This is so cool! I want this for every language now.
you stick this in your struct
type noCopy struct{}
func (*noCopy) Lock() {}
func (*noCopy) Unlock() {}we're still inventing languages where local variables can be mutated
Local mutability is probably one of the most common uses of mutability. A lot of it is using local state to build up a more complicated structure, and then getting rid of that state. Getting rid of that use-case is just giving up performance.