nextos

47 ms·

751.
by nextos 3y ago
Good point. My main distro is NixOS, so I am not too familiar with Guix. After a quick glance at the code, Guix seems to be similar to bwrap et al. as it uses kernel namespaces for sandboxing [1]. I think the pure option is not really for (
752.
by nextos 3y ago
It's an interesting endeavor, but there are some obvious safety concerns. Within Prokaryotes, there is a lot of horizontal gene transfer. What if some of the synthetic sequences get into other organisms and spread out?
753.
by nextos 3y ago
See https://guix.gnu.org/manual/en/html_node/Invoking-guix-shell... It's a sandboxing feature similar to e.g. Firejail. One can launch applications in a separate container, and choose whether to give acc
754.
by nextos 3y ago
An interesting advantage of Guix over Nix is having better options for runtime isolation. Nix is not well developed in this area yet, although one can always use bwrap or AppArmor to implement something ad hoc. Besides, Guix uses Scheme eve
755.
by nextos 3y ago
I don't think this is entirely true. Most heavy-tailed distributions make CLT convergence slow , and heavy-tailedness is relatively common. Many methods in finance and pharmacology, just to give two examples, have had spectacular fail
756.
by nextos 3y ago
While the OP might want to upgrade his mum's laptop, it should be noted that an old MacBook can run any current Linux distribution. These will offer the latest software, and will be able to do Internet banking without any issues, obvio
757.
by nextos 3y ago
Also there are great fanless cases for NUCs and RPis. Actually, Asus has taken over NUCs from Intel and they are releasing fanless machines, so now there is not even the need to mod them.
758.
by nextos 3y ago
Indeed, for a small country in terms of population, they have a really impressive defense industry. Also a very interesting distributed defense doctrine: https://en.wikipedia.org/wiki/Bas_90
759.
by nextos 3y ago
Do you use Copilot on a language equipped with refinement or dependent types, and use said types to constrain generation of entire functions, in a single step, that are also formally verified?
760.
by nextos 3y ago
Lots of related work also by A. Solar-Lezama https://people.csail.mit.edu/asolar , sometimes in collaboration with N. Polikarpova.
761.
by nextos 3y ago
Decoupling both is the simplest option, but not the one I am focusing on. Also note SAT/SMT can also be used for synthesis. In fact, synthesis has a relatively rich history using SAT/SMT solvers.
762.
by nextos 3y ago
Not yet, it's a bit rough. The LLM I am using requires a bit of extra fine-tuning to be really smooth, I need to rent a bigger GPU. Besides, I am working on some novel integration between transformers and SAT/SMT that will take me
763.
by nextos 3y ago
IMHO, in the future programming may look similar to this. Write a type declaration for a function with an expressive type system, e.g. refinement types. Then use LLMs + SAT/SMT to generate provably correct code. This strikes a happy me
764.
by nextos 3y ago
EU mandates storm retention tanks, i.e. a buffer, to minimize this problem. For instance, Madrid has built a massive 400,000 m3 tank and the problem is now solved. Lots of other main cities are doing / have done the same. Without those
765.
by nextos 3y ago
Unfortunately, Thames Water infrastructure, once state-of-the-art, is really old and it shows. It needs some serious investment to bring it to modern standards. In Oxford, I have noticed raw sewage floating in the river several times. Thing
766.
by nextos 3y ago
He has also published The Book of Shen , which is really interesting. Sadly, the lack of extensive free documentation is probably harming Shen's popularity.
767.
by nextos 3y ago
The main strategy is to build sound but imperfect analyzers, i.e. analyzers that never raise false negatives but that may raise some false positives. See §1.6 in [1], a simplified version of the classic Principles of Program Analysis . Goo
768.
by nextos 3y ago
Yes, most free lunch theorems and results of this kind, which make overly general assumptions, tend to be too pessimistic. For example, many people naively think that static program analysis is unfeasible due to the halting problem, Rice&#x
769.
by nextos 3y ago
Same here. I think Apple Watch is their best product, and it has a lot of potential as a biomarker monitor, e.g. to measure insulin.
770.
Creusot, a deductive verifier for Rust code(github.com)
3 points by nextos 3y ago|0 comments
771.
by nextos 3y ago
Also, related HN thread: https://news.ycombinator.com/item?id=24056901
772.
by nextos 3y ago
This led to the algebra of programming school: https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/s... For context, see this discussion: https://stackoverflow.com/questions/567127
773.
by nextos 3y ago
Nix works wonderfully well for this. As a bonus, it will solve the problem not only for Python, but also for any other dependencies you may have. The only two package managers that have never given me a single headache when installing Pyt
774.
by nextos 3y ago
I think the real power will come when generative models get combined with e.g. refinement types, which are more or less analogous to contracts. Imagine, you decompose a problem into some functions with some contracts, and you get implementa
775.
by nextos 3y ago
Simple Haskell could be a thing, there have been some efforts in the community but none really crystalized. Frankly, I don't think the problem is so much difficult I/O, but rather too many language extensions, competing toolchains
776.
by nextos 3y ago
There are also Russians staying in Russia who try to fight the regime from inside, and that is also a morally correct approach to things. Actually, given Russia is supported by other countries including PRC, I think Putin's regime is m
777.
by nextos 3y ago
I prefer Gelman, Hill & Vehtari Regression and Other Stories (ROS). It's also free: https://avehtari.github.io/ROS-Examples . It's a great prequel to Gelman et al. Bayesian Data Analysis (BDA). I have a formal
778.
by nextos 3y ago
Same experience here. As a small organization, the quotes we got from cloud providers have always been prohibitively expensive compared to running things locally, even when we accounted for geographical redundancy, generous labor costs, etc
779.
by nextos 3y ago
There are serious clinical trials with randomization and placebo that have repeatedly shown vitamin D supplementation reduces autoimmune disease rate. For example [1]. Obviously, the effect of a compound that does not require prescription a
780.
by nextos 3y ago
Also you can't operate e.g. a dishwasher with kitchen gloves now, as those silly touchscreens won't cooperate. Few brands know how to keep it simple. Even Miele and Liebherr are falling into these absurd trends.

More ›