nextos

25 ms·

391.
by nextos 2y ago
The good thing about Wayland is that security is much better. In X, a compromised application can easily steal information. Sandboxing is hard. The bad thing about Wayland is that changes to the architecture are incompatible with window man
392.
by nextos 2y ago
To some extent, this also applies to software. Except for DeepMind and a few other select places like Altos Labs, getting past £100k is hard , especially outside London. Unless you go into finance, of course. But then, you have to stick to
393.
by nextos 2y ago
The Lumia was essentially a N9 ported from Linux to Windows. The N9 was the best phone I have ever owned. The UI was fantastic. In particular, the offline navigation application was incredible. Nokia could have succeeded in the smartphone m
394.
by nextos 2y ago
> Better tooling is an exponent to our productivity Nix & NixOS have made me much more productive. Maintaining a desktop is effortless. If something breaks, I can simply reboot to a previous installation. I can also try software wi
395.
by nextos 2y ago
Simon Peyton Jones is a relatively recent example of someone who went from BSc in Cambridge, to a lectureship and eventually a professorship, without a PhD: https://en.wikipedia.org/wiki/Simon_Peyton_Jones#Education
396.
by nextos 2y ago
This is also my take on this. IMHO, LLMs + theorem provers have the potential to make formal methods cheap enough to use more widely. And we should give more credit to the theorem prover part of the equation, which comes in part from old AI
397.
by nextos 2y ago
Lean has very little support for proving things about software. Right now, the community is mainly geared towards mathematics. This could change. Concrete Semantics was rewritten in Lean [1], but I haven't seen more efforts geared to
398.
by nextos 2y ago
Sure, what I meant is that Dafny outsources everything to SAT/SMT. If it doesn't manage to prove things for you, it gets a bit frustrating as there is not much support for manual tactics compared to F*, Coq or Isabelle, which can
399.
by nextos 2y ago
Having used both Dafny and F* quite extensively, Dafny, and its predecessor Spec#, are simple and practical, thanks to being based on Hoare logic (contracts). It's a great place to start with verification, as proofs are discharged to S
400.
by nextos 2y ago
> My position was that DL isn’t sufficient - we need a forward looking RL streaming reward system [...] I agree, but don't you think some degree of symbolism or abstraction building is necessary for AGI? Current systems seem to be t
401.
by nextos 2y ago
Haskell could be a great practical language if some constraints were introduced, e.g. limiting the language extensions used. https://www.simplehaskell.org attempted to do this and, currently, https://neohaskell.org i
402.
by nextos 2y ago
Perplexity, Phind, Grok, etc. are surprisingly good already as search engines. Perplexity is better than Google for most of my common use-cases.
403.
by nextos 2y ago
With the Linux kernel, USB power savings are also annoying on Logitech devices. If you set everything on USB bus to powersave, their mice and keyboards will go to sleep every few seconds unless there's continuous activity. I have exper
404.
by nextos 2y ago
The pMHC-TCR complex, which is the cornerstone of the adaptive immune system, has evolved to bind peptide epitopes. Most D-amino acids are known to bind MHC poorly and lead to reduced TCR recognition. I imagine this could increase the chanc
405.
by nextos 2y ago
Local momentum I guess. Lots of non-tech SMEs in the UK use Ubuntu since the 2010s. Another factor is Office interop, especially Excel. Office 365 has simplified that, but it's still far from perfect. Personally, I think non-tech SMEs
406.
by nextos 2y ago
It's still the very best for symbolic math. But it has fallen behind on other domains. And even in the symbolic math niche, I am afraid that Python and Julia will slowly erode its market-share.
407.
by nextos 2y ago
A Pixel is great to use GrapheneOS, i.e. Android sans Google. For stock or nearly stock Android, other options are more cost-effective.
408.
by nextos 2y ago
With a bit of creativity you can run something similar for free. It's worth noting Raspberry Pi comes with a free Wolfram license. The assistant part can come from something like Perplexity, which in my experience is decent at writing
409.
by nextos 2y ago
Install Nix and you can launch Nyxt, and many other things, without even installing them in Debian. In case of Nyxt, once Nix is installed, just run nix run nixpkgs#nyxt.
410.
by nextos 2y ago
I used Greasemonkey for some time. What do you find ViolentMonkey useful for these days?
411.
by nextos 2y ago
OP here, running an i5-4250U. A 10-11 year old low-power CPU and a SATA SSD, definitely quite slow by current standards.
412.
by nextos 2y ago
Nyxt is very promising, and I hope it gains momentum. The obvious advantage of Nyxt is programmability and keyboard-driven workflows. However, I use old hardware, and it's a bit slow and laggy. Chromium behaves the same way, so I imagi
413.
by nextos 2y ago
Or Ruby, which is essentially Smalltalk for Unix, plus lots of Perl-isms. Haskell (e.g. shh) and Clojure (Babashka) are also a nice for this usecase, but more niche options.
414.
by nextos 2y ago
I use Firejail in the terminal as I am also concerned with the things you mentioned. bwrap is also a possibility. For simple usecases, they are not too intrusive. You can easily create a development profile that bans internet access and for
415.
by nextos 2y ago
I just use the "net none" option. For the rest of the programs, Firejail default profiles are spot on. Alternatively, you can use bwrap --share-net=none emacs.
416.
by nextos 2y ago
That's my opinion as well. I run Emacs 24/7 but I do so inside Firejail, with no network access. It's not architected with security in mind and exploits are too easy. The same can be said about the Linux userland. The Unix mo
417.
by nextos 2y ago
Static types do provide some guarantees as they rule out an entire class of runtime errors. In case of XMonad, since Haskell's type system is more expressive, the class of runtime errors ruled out at compile-time is broader.
418.
by nextos 2y ago
Sure, my statement referred to dwm, and it also applies to XMonad.
419.
by nextos 2y ago
Sounds scary but it's giving you some compile-time guarantees about correctness. StumpWM and XMonad do the same and they are quite easy to use, especially the former. They also lead to very space-efficient setups. Windows can be tightl
420.
by nextos 2y ago
Oxford doesn't pay staff well unless you are in the top of the pyramid, i.e. a professor. Paradoxically those tend to contribute less to education. Senior postdocs and fellows do a significant amount of teaching but their salaries are

More ›