I don't think he touched on whether server side is a more valid use case, but was nice to read someone elses take on using it for a desktop. Thanks for the contribution.
He did find functional programming to be sort of mystic so I don't know if I trust his take on assesing the nix language itself.
TLDR; just stick with ubuntu or arch unless you feel like experimenting
Author here. Your TLDR is spot on. Yes, my intent was to be on desktop use since most things I read dont consider that specifically.
I did talk about how I would keep this running on some simple home servers since I think that's where Nix shines. But some of my servers are raspberry pis, which I mentioned I am worried to run Nix on due to resource limitations. I should probably just try it.
I'm running NixOS on a raspberry pi and I deploy to it with deploy-rs¹. This works pretty well for me. My dev machine is an Apple Silicon laptop with nix-darwin installed and I use its nix.linux-builder module to run an aarch64-linux VM as a remote builder to build the rpi's system. All this means the rpi never has to do any building itself, and doesn't even need the nixpkgs source installed either.
If you want to do this yourself, I recommend using https://github.com/nix-community/raspberry-pi-nix so the system is configured much more closely to how the stock raspberry pi image works. The benefit of this is better reliability of stuff like bluetooth.
It might be technically true, but I don't think it would be true in practice. The difference is that:
- Technically true means you will probably win any lawsuit they bring
- In practice means that they will in fact bring a lot of lawsuits, making it very expensive for you and difficult for you to operate. They will probably find excuses to harass you over every little thing, they will harass you over lots of details that are technically required but rarely enforced in practice. You'll constantly be getting inspected and audited, they will bring lawsuits for other, apparently unrelated things.
What, to you, is an ultra strong type system? Both OCaml and Haskell are used in plenty of non academic contexts. Do you mean something like Coq or F*?
I don't see many GAFAM products created in any functional language, even those with primitive type systems. Are you sure it is the type system that is scaring people away?
Oh that's a solved problem since 1969. It's called "unix". Everything is a file which can be processed as a byte stream. Composition is a breeze- can't be any more general than that!
An actual Lisp programmer will tell you that the right thing depends on the situation. The right thing can be a lambda, a string, a symbol, a structure, a class object, a hash table, a vector, a list, a call to a foreign function, a syntactic abstraction, a bitmask, a load-time value, a pattern matcher, ...
I am not convinced about that. I think that many people discovered the notion of "memory safety" with Rust, and think that only Rust provides it. The grandparent is right: Rust brings memory safety at low cost, that's the whole point.
Correct me if I'm wrong (I've only dabbled in F* and only briefly read about 1ML) but wouldn't F*'s full dependent types make 1ML redundant?
That is, once you've brought types into the value level, modules themselves become redundant - they're just records, and functors are just functions. The point of 1ML, IIUC, is to accomplish a similar unification without demanding full dependent types and the attendant complexities they bring.
Interesting point. I never inferred a strong connection between dependent types and the unification of records and modules. Maybe a real PL theorist around here can provide insights on that subject.
reply