Berdes's recent activity
-
Comment on AI models may be capable of self-replicating without access to a datacenter in ~tech
-
Comment on Given everything we know about AI so far, what do you think it can or cannot be good for? in ~tech
Berdes Link ParentCorrection: it has been configured to please users. I have zero doubts that LLMs get optimized/tuned exactly the same way that social media have been optimized to be as addictive as possible, with...it wants to please user
Correction: it has been configured to please users. I have zero doubts that LLMs get optimized/tuned exactly the same way that social media have been optimized to be as addictive as possible, with no regards for any the negative impact they might have on users.
-
Comment on Given everything we know about AI so far, what do you think it can or cannot be good for? in ~tech
Berdes LinkI think there is a clear pattern where the usefulness of LLMs scales with how easily their output can be verified. The easiest being when the verification can be done automatically, such as code...I think there is a clear pattern where the usefulness of LLMs scales with how easily their output can be verified. The easiest being when the verification can be done automatically, such as code being compiled and tested or math proofs being checked with something like Lean. This will certainly speed up some tasks, but I doubt that most jobs consist of doing only that.
There are two things I have in mind where I think LLMs could be really useful tools that haven't been explored all that much so far (or at least I'm not aware of that). The first one is about proving software. A lot of bugs and security vulnerabilities come from stuff like buffer overflows, dereferencing null pointers and more generally invariants being violated. In my opinion, safer languages like Rust fall short on two aspects: they will rejects programs that are provably safe (sometimes trivially so) and they only check a small subset of issues with no way for programmers to extend what is being checked. More general approaches, where people can add verified annotation for any provable properties would be the logical next step. So far, this kind of approach was way too labor-intensive to make sense for almost all software, but I hope LLMs will help reduce this cost to make this approach more common.
The second thing that I think LLMs could help with is making interaction with complex software easier for casual users. As an example, I use Gimp every couple of months to do some basic image editing. Because of this low frequency, I will never build enough habit to be really efficient and I think that having an LLM translate human language into whatever the software understands could really help here. Importantly, I think that having a more structured output for the LLMs should reduce the risk of unwanted effects compared to asking a multimodal model.
On the other hand, hallucination and mistakes that basically no human would make are still a problem. For example, I recently had a model (I think GPT-6 Luna) casually drop something like "that was 17 months ago, so not quite a year" in the middle of an answer. I don't know if we will ever reach a point where this happens rarely enough that it won't affect the quality of outputs.
-
Comment on Finding bugs in Raft implementations in ~comp
Berdes Link ParentThat's a totally fair point. While the OS or even some aspects of the hardware could be part of the thing you prove, there is pretty much always something outside of that boundary that can still...That's a totally fair point. While the OS or even some aspects of the hardware could be part of the thing you prove, there is pretty much always something outside of that boundary that can still mess things up (a cosmic ray flipping some bits, a grid voltage fluctuation causing unpredictable stuff to hapen in the CPU, undesirable quantum stuff, etc).
The original comment mentioned unit testing, and it's supposed to test code in isolation. So one could argue that proving that the code will pass the test fulfills the point of unit testing. But I don't think any sane person will fully isolate the piece of code being tested (for example, when you run it, you still rely on the OS doing proper memory management, if you call sort(), you're not going to mock that, erc...). And in my experience, it can be more useful for the "unit test" to include as many things in the test as possible as long as it doesn't make the test too slow or too complex, because that provides more testing for the other parts if the system.
-
Comment on Finding bugs in Raft implementations in ~comp
Berdes Link ParentI'll try to answer your questions as best as I can. Just keep in mind it's only a subjet I'm interested in (and had a class 10+ years ago), but I'm not a professional in the field. Also, I have a...I'll try to answer your questions as best as I can. Just keep in mind it's only a subjet I'm interested in (and had a class 10+ years ago), but I'm not a professional in the field. Also, I have a more software engineer point of view of formal verification, rather than a mathematician one. I have written a lot of code that IMHO would benefit tremendously from having some properties formally verified, but I haven't really designed anything where you have specs complex enough (and critical enough) that formal verification for the specs would make sense.
-
If you have separate specs and implementation, you can't really ensure that they match, unless you program the implementation in a language that has built-in formal verification (like Lean) and can be certain you mirrored the specs correctly. But at that point, it might be simpler and safer to just do everything in the language you're using. In some cases, it can still be useful to prove the specs without being certain the implementation matches. It really depends on how certain you want to be that your program is "bug-free".
-
You can prove a lot of useful stuff, even for a web app. Typically, you might have some parts of the app that require stuff that cannot be modeled by the type system (or at least, bot efficiently). Pre-conditions of functions/methods are stuff that are often up to programmers to ensure, but you would prevent a lot of bugs if you could ensure they are never violated. Ensuring your vector/array has at least n elements when accessing the nth, or not dereferencing a null pointer are examples of such pre-conditions. On a larger scale you might also want to ensure that you never leave your database in a "bad state" (e.g. with invariants violated) as a result of a request or transaction. However, I don't think you can ever prove that a program is "bug-free", as you can't really formalize what a "bug" is. At best, you can ensure your program is free of some classes of bugs (like buffer overflows) and has some specific properties.
-
In theory, you could replace all software testing with formal verification. If you prove that your test will pass, there is no need for running it. In practice, running the test might be a while lot faster than checking that the proof is correct. There are also cases where you juge that the guarantees you get from formal verification are not worth the effort.
-
-
Comment on What have you been listening to this week? in ~music
Berdes LinkCantus arcticus Op. 61 composed by Einojuhani Rautavaara. This is a 3-parts orchestral work in a contemporary classical style. Unlike a lot of music in this style, I found it super interesting and...Cantus arcticus Op. 61 composed by Einojuhani Rautavaara. This is a 3-parts orchestral work in a contemporary classical style. Unlike a lot of music in this style, I found it super interesting and enjoyable to listen to. One of the most notable element of this work is that it's using recordings of bird songs. They are not present all the time, it's more like one or a few birds are passing by and make their voice heard before moving on.
I was also surprised to see that the composer is more well known than I would have initially expected. Or more exactly, there are somewhat frequent representations of his works when looking at the whole world. I'm seeing almost 10 concerts in the next year, while some other "niche" composers I've looked at are barely played than once or twice a year worldwide.
-
Comment on What games have you been playing, and what's your opinion on them? in ~games
Berdes (edited )LinkI picked up Silksong recently, now that the hype died down and most issues/bugs should have been fixed. Similarly to Hollow Knight, I found some parts amazing and some parts needlessly...I picked up Silksong recently, now that the hype died down and most issues/bugs should have been fixed. Similarly to Hollow Knight, I found some parts amazing and some parts needlessly difficult/punishing.
Typically, I'm not a huge fan of boss fights that are very chaotic or that pretty much require spamming tools, and there are a few of those. Arena fights often falls under this category, but some bosses alos spaws smaller enemies. In those cases, I find it incredibly difficult to "learn" the fights, making them difficult, without the feeling of accomplishment once I finally win.
The system of crests is quite interesting. I've done almost everything using the reaper crest, since it's easy for platforming and generate enough silk to heal a lot. However, for the more difficult bosses near the end of act 2 and act 3, I'm often trying out different crests with vastly different success. For example, I found the hunter crest really usefull for the Karmelita fight.
-
Comment on Apple announces significant price increases for MacBooks, iPads, more in ~tech
Berdes Link ParentThe problem is that for anything that runs on people's devices, developpers have almost no incentive to optimize anything beyond the absolute bare minimum of making it work on most low end devices...The problem is that for anything that runs on people's devices, developpers have almost no incentive to optimize anything beyond the absolute bare minimum of making it work on most low end devices under favorable circumstances.
because of this, the only way for apps and websites to be well optimized is to have the devs working on them to be sufficiently knowledge, interrested and to have enough choice about what this can work on to be able to pick optimisation work insted of working on the next feature/app. -
Comment on Around twenty drown in France as French seek relief from heatwave in ~enviro
Berdes Link Parent30°C at night sounds like a nightmare compared to the 42 during the day. When I used to live in the south, the main thing that helped during heatwave was the low night temperature, which allowed...30°C at night sounds like a nightmare compared to the 42 during the day. When I used to live in the south, the main thing that helped during heatwave was the low night temperature, which allowed us to cool down the house and keep things tolerable during the day. At 30, that's hardly possible.
-
Comment on Almost half of EU’s busiest flight routes are ‘hard or impossible’ to book on trains in ~transport
Berdes Link ParentFiguring out good cross-border train options have been a significant hurdle for me multiple times. When you compare how easy it is to search for flights on Google Flight vs any train booking apps,...Figuring out good cross-border train options have been a significant hurdle for me multiple times. When you compare how easy it is to search for flights on Google Flight vs any train booking apps, the difference is massive. This is especially true for cases where you're flexible on time, date and/or specific train stations.
Before even considering an eco tax, making sure flight tickets don't skip taxes like VAT would be a good first step IMHO.
But by far the biggest decider for me between a flight and a train have been price and availability. Very often, a train would be 300+€, with potentially no availability already 1 month in advance, while I can usually book a flight for half the price 2 weeks in advace. Without adressing this kind of differences, I don't see how train travel can hope to replace fights within the EU.
-
Comment on ‘I took two bites and had to spit it out’: US candy makers are phasing out real cocoa in chocolate in some products in ~food
Berdes Link ParentI don't remember if I already tried Dandelion, but I recognize the name from various bean-to-bar stores I went to and would generally recommend anything bean-to-bar. More specifically, here is a...I don't remember if I already tried Dandelion, but I recognize the name from various bean-to-bar stores I went to and would generally recommend anything bean-to-bar.
More specifically, here is a small selection of the ones I tried and would gladly recommend:
- Made in USA: Amano and Fruition.
- Made in Canada: Quantu and Sirene
- Chocolate makers using cacao from their own country: Luisa Abram (Brazil, best chocolate I've ever eaten), Fu Wan (Taiwan), Chocolat Madagascar (Madagascar, obviously), Marou (Vietnam, the company itself is French, but the cacao is sourced from Vietnam and the chocolate is made there). You should find an importer for those ones since I don't think any of them ship internationally to individuals.
For those kind of producers, dark chocolate in the 60% to 80% range are the most common and are a good starting point if you want to explore the space. Some also make dark milk versions, which also have a high percentage of cacao. By definition, the difference between dark chocolate and milk chocolate is that milk chocolate also contains milk powder. So it's totally possible to have milk chocolate that is no more sweet than dark chocolate. Finally, you have chocolate made with some additional ingredients. That's where chocolate makers can be very creative. For example, Fu Wan makes some tea-infused chocolate (those are absolutely delicious).
If you're new to this space, I would also recommend tasting those chocolate by just getting a small piece and letting it melt in your mouth instead of chewing it. That's how you get the most of them. The main exception are the bars with inclusions (stuff like cacao nibs), that often have a more balanced tasting profile when you chew the inclusions while the chocolate is melting in your mouth.
Outside of the recommendations I made above, I would also trust any chocolate who received an Academy of Chocolate award or an International Chocolate Awards. Such bars will have a logo of the award(s) on them.
-
Comment on 'They've probably been untouched for 49 million years': The New Mexico cave expanding our search for alien life in ~science
Berdes Link ParentI found a research paper (Life in the dark: far-red absorbing cyanobacteria extend photic zones deep into terrestrial caves, full PDF accesssible on Google Scholar), which matches pretty well what...I found a research paper (Life in the dark: far-red absorbing cyanobacteria extend photic zones deep into terrestrial caves, full PDF accesssible on Google Scholar), which matches pretty well what is described in the article. At the very beginning of the result section, they talk about 4 different caves:
We investigated four caves within Carlsbad Caverns National Park that were predominantly formed in the Capitan Formation of the Delaware Basin [...]. The entrance morphology and direction of each cave varies;
That could easily explain some of the discrepancies about when the caves where formed and when the entrances where opened.
Also, in the previous paragraph (emphasis mine):
To investigate the occurrence and distribution of far-red–absorbing chlorophylls in cave ecosystems, we studied the microbial communities and their photo-pigmentation along longitudinal light gradients of four cave entrances, which have likely existed in their present form for the last 4–9 million years.
I might be completely wrong here, but I feel like the "49 million years" in the article title could be a typo or misunderstanding from the "4–9 million years" in the paper. Forty-nine and four to nine can sound very similar, especially if some non-native speakers are involved. This would be a pretty embarrassing mistake if true, but one that sounds plausible to me.
-
Comment on Microsoft has killed widgets six times. Here's why they keep coming back. in ~tech
Berdes LinkI feel like the design ethos for many widgets is form over function: they look cool and/or pretty, but end up taking a lot of space with very little information density. Why would I want to...I feel like the design ethos for many widgets is form over function: they look cool and/or pretty, but end up taking a lot of space with very little information density. Why would I want to dedicate 1/10th of my screen to have the current time, when all the information can be tucked away in a qmall corner of the screen? This ends up leading to widgets being hidden most of the time, defeating the "getting information at a glance" part of the requirements for them to be really useful.
-
Comment on Hacktivist deletes three white supremacist websites live onstage during hacker conference in ~tech
Berdes Link ParentEven though I hate white supremacist views, I don't think this is the right way to deal with the problem. IMHO, either their views are sufficiently detrimental to society to be forbidden to be...Even though I hate white supremacist views, I don't think this is the right way to deal with the problem. IMHO, either their views are sufficiently detrimental to society to be forbidden to be broadcasted on the public square, in which case the justice system/executive should deal with it. Or, the websites should stay online and not face attacks from random people.
While outlawing this kind of content would be an infringement to freedom of speech, I do think this can be morally justified. Even in the US, where freedom of speech is often said to be great, there are numerous restrictions to it: defamation, copyright, trade secrets, national security, terrorist threats, false advertising, etc.
There are obviously more nuances to be had in cases where such content is hosted in a country that doesn't want to censor it.
-
Comment on Food: Your personal year in review for 2025 in ~food
Berdes LinkThe best food I had this year was black cod dish, where the fish had been marinated in a miso sauce and later cooked on the flame (japanese technique named robotayaki). This was part of a tasting...The best food I had this year was black cod dish, where the fish had been marinated in a miso sauce and later cooked on the flame (japanese technique named robotayaki). This was part of a tasting menu, where every single dish was delicious, even though I clearly had my favorite.
My favorite meal was something I started cooking this year. Not sure how to describe it exactly. It's kind of like a curry but with way less sauce rhan a typical curry, I'm using onions, carrots, tomatoes, fresh curcuma, cayenne pepper, paprika and nutmeg for the base (cooked long enough that they basically from a sauce), tempeh for the proteins and near the end, I add some bell pepper, zuccini and mushrooms, all 3 cooked just enough to be not be raw while keeping their texture. I always eat this whith rice, of course. Interestingly, my first try didn't have the tomatoes and I was super happy when I figured out that what I felt was mussing was just some acidity, which can easily be added with something like tomatoes.
On the baking side, I learned to make bread. My first attempt went surprising well. I used some basic white flour and instant yeast (which are both far from ideal), but the result was still better that the garbage that Dutch supermakets have the audacity of calling "bread". Obviously, my technique improved and I'm now usually using a mix of spelt flour and whole wheat, with sourdough starter and a bit of instant yeast to ensure I'll still always have a good result.
I had a minor disaster with the dish described above, when I tried some fresh peppers to replace the cayenne powder. The mix I bought included a habanero pepper, and even just half made the dish almost too spicy for me to be able to eat it. It tasted like a raging fire, with a slight hint of what I normally expect from the dish.
-
Comment on Linus Åkesson - 8-bit Boléro (2025) in ~music
Berdes LinkWhile it's a pretty interesting interpretation, the answer to the title question (The World's Most Ambitious Chiptune?) is a clear "no" IMHO. I'm at least aware of the Super Rite of Spring by...While it's a pretty interesting interpretation, the answer to the title question (The World's Most Ambitious Chiptune?) is a clear "no" IMHO. I'm at least aware of the Super Rite of Spring by Shabubula (which is critically under-viewed!) that seems way more ambitious to me, and there might be even more out there.
-
Comment on EU drops 2035 combustion engine ban as global electric vehicle shift faces reset in ~transport
Berdes Link ParentYou can go even further and get rid of the frame, add a smidge of human power and you end up with an e-bike! This would also reduce the parking space need, reducing distance between destinations,...You can go even further and get rid of the frame, add a smidge of human power and you end up with an e-bike! This would also reduce the parking space need, reducing distance between destinations, counteracting part of the time lost due to the speed reduction.
-
Comment on EU drops 2035 combustion engine ban as global electric vehicle shift faces reset in ~transport
Berdes Link ParentAnd that's not restricted to taxis. If parents need to do a return trip (or a significant detour) to bring/pick up their kids from school and other activities, they are also unnecessary overhead....And that's not restricted to taxis. If parents need to do a return trip (or a significant detour) to bring/pick up their kids from school and other activities, they are also unnecessary overhead.
But I also think that in most cases, driverless taxis should be the last resort solution for cases when a better approach (public transport) cannot work.
-
Comment on AI-designed Linux computer with 843 components boots on first attempt — dual-PCB Project Speedrun was made in just one week and required less than forty hours of human work in ~tech
Berdes Link ParentFrom what I can see, it's only an "AI" because of the hype around the term. They talk about it doing some placement and routing tasks, which is something that can be done by existing tools. Maybe...From what I can see, it's only an "AI" because of the hype around the term. They talk about it doing some placement and routing tasks, which is something that can be done by existing tools. Maybe it's doing a bit more than existing competitors?
About the project they present, I saw some feedback from someone working in the industry (on a different website) and their conclusion was that the project was perfectly scoped to magnify the impact of their tooI. For example, they don't start from scratch, but reuse an existing design (which can take 1-2 months of work for this kind of design). They also use a service to get an extra-speedy manufacturing of the board, which most people wouldn't use due to the cost. Testing (beyond just booting an OS) is not included either. So basically, their tool speeds up a small part of a hardware engineer job when compared to it being done manually. Without a proper comparison against similar tools, their advertisement is pretty meaningless.
-
Comment on Day 12: Christmas Tree Farm in ~comp.advent_of_code
Berdes LinkI got baited soooooo hard by this problem. I started implementing a solver for the general problem, believing that maybe the dimensions where small enough that a good implementation could work....I got baited soooooo hard by this problem. I started implementing a solver for the general problem, believing that maybe the dimensions where small enough that a good implementation could work. Obviously, I had a very quick explosion of states while trying to find a solution for any of the regions. So I implemented some additional logic to try and eliminate states that are strictly worse than other states I generated, which still wasn't enough. So I looked at culling states that had no hope of being filled and early exiting if I found a state that could trivially finish being filled. Magically, those two last optimizations where enough... because every single input immediately fits into one of those categories.
Also, while trying some manual inputs with feasible dimensions, I saw that my solver clearly had some bugs because it could find a solution for a 39x6 region, but not for a 40x6 with the exact same shape requirements. :|
Anyway, if anyone is interested, here is my solution after angrily deleting all the code related to the useless solver (there are still traces of optimizations that are clearly not necessary anymore):
Solution (Rust)
use aoc_2025::timed_run; use std::io; use std::vec::Vec; // Bitmask of the shape. Bit 0 is the top left, bit 2 the top right and bit 8 the bottom right. #[derive(Clone, Copy)] struct Shape(u16); impl Shape { fn parse(ls: &[String]) -> Self { assert_eq!(ls.len(), 4); let mut ret = 0; let mut pos = 0; for x in 1..4 { assert_eq!(ls[x].len(), 3); for c in ls[x].chars() { match c { '#' => ret |= 1 << pos, '.' => {} _ => panic!("unexpected char {} in shape", c), } pos += 1; } } Shape(ret) } #[allow(dead_code)] fn to_string(&self) -> String { let mut ret = String::new(); let mut tmp = self.0; for i in 0..9 { ret.push(if tmp & 1 == 1 { '#' } else { '.' }); if i == 2 || i == 5 { ret.push('\n'); } tmp >>= 1; } ret } } struct Region { width: u32, height: u32, shapes_count: Vec<u32>, } impl Region { fn parse(l: &str) -> Self { let (size, shapes) = l.split_once(": ").unwrap(); let (width, height) = size.split_once('x').unwrap(); Self { width: width.parse().unwrap(), height: height.parse().unwrap(), shapes_count: shapes .split(' ') .map(|s| s.parse::<u32>().unwrap()) .collect(), } } #[allow(dead_code)] fn to_string(&self) -> String { format!("{}x{}: {:?}", self.width, self.height, self.shapes_count) } fn trivial_fit(&self, shapes: &Vec<Shape>) -> Option<bool> { let num_trivial_shapes = (self.height / 3) * (self.width / 3); let num_required_shapes = self.shapes_count.iter().fold(0, |a, b| a + b); if num_required_shapes <= num_trivial_shapes { return Some(true); } let num_required_spots = shapes .iter() .map(|shape| shape.0.count_ones()) .zip(self.shapes_count.iter()) .map(|(a, b)| a * b) .fold(0, |a, b| a + b); if num_required_spots > self.height * self.width { return Some(false); } None } } struct Input { shapes: Vec<Shape>, regions: Vec<Region>, } impl Input { fn read_from_stdin() -> Input { let lines = io::stdin().lines().map(|l| l.unwrap()).collect::<Vec<_>>(); let mut iter = lines.rsplit(|l| l == ""); let regions = iter .next() .unwrap() .iter() .map(|r| Region::parse(r)) .collect::<Vec<_>>(); let shapes = iter.map(|ls| Shape::parse(ls)).rev().collect::<Vec<_>>(); for r in ®ions { assert_eq!(r.shapes_count.len(), shapes.len()); assert!(r.height > 2); assert!(r.width > 2); } Input { shapes, regions } } } fn part1(input: &Input) -> u64 { let mut ret = 0; for r in &input.regions { match r.trivial_fit(&input.shapes) { Some(true) => ret += 1, Some(false) => {} None => panic!("Cannot trivially solve {}", r.to_string()), } } ret } fn part2(_input: &Input) -> u64 { 0 } fn main() { let input = Input::read_from_stdin(); timed_run("Part 1", || part1(&input)); timed_run("Part 2", || part2(&input)); }
How can AI inference be significantly locked down? To me, this sounds about as impossible as locking down modern cryptography. The only way I see would be to prevent people from owning computers or anything that can perform significant amount of computation and and that's just not realistic.
IMHO, what we need is a global push towards writing software that is less blatantly unsecure. Unfortunately, I have the impression that we're currently going in the opposite direction, with more and more software being vibe-coded with no or very limited review.