Posts by dlakelan@mastodon.sdf.org
 (DIR) Post #B4t05uTt4tbbv3W1D6 by dlakelan@mastodon.sdf.org
       0 likes, 0 repeats
       
       @linear @cwebber I'd set aside the formal verification requirement to get the rest of it. I really do think microkernels were the right way to go, it's just that in 1992 or whatever the consumer hardware wasn't up to the task. I think probably around 2005 or so the hardware started to be able to afford to do that. But that's approximately the time that VMs and containers took off. Now we have this giant mess.
       
 (DIR) Post #B4t13LeFiMSXGJhpTM by dlakelan@mastodon.sdf.org
       0 likes, 0 repeats
       
       @linear @cwebber If you mean formally verifying the microkernel itself... yeah. I'm good with that. Isn't L4 formally verified? If you mean formally verifying every userspace daemon... Nice to have but I'm not holding my breath.
       
 (DIR) Post #B4t4IUIU8k66ICR2S8 by dlakelan@mastodon.sdf.org
       0 likes, 0 repeats
       
       @linear @cwebber I agree it would be nice to have, but I honestly think it primarily prevents progress. We'd be wildly better off with microkernel OSes that are at the same level of hackiness as the Linux kernel, and maybe have decent interfaces that could get replaced piecemeal as people came up with alternative implementations in memory safe languages, and then maybe formally verified at a later date. Right now, you have to be comfortable working in kernel space to even do anything
       
 (DIR) Post #B4t5EevUmLvM3QQ6tc by dlakelan@mastodon.sdf.org
       0 likes, 0 repeats
       
       @linear @cwebber That's cool! I honestly had not followed any of this. I might have to dedicate an older laptop I have no real use for to this just for fun.
       
 (DIR) Post #B58oZtyjQ8e67xpuE4 by dlakelan@mastodon.sdf.org
       0 likes, 0 repeats
       
       Today was a good day. A tiny bit of #anarchist university happened. Specifically my older son has this personal project due for IB 10th grade, and his project is to investigate how climbing chalk benefits rock climbers. So we've got this little apparatus to investigate the friction properties of little patches of leather on a sandstone flagstone from the front yard. before the CO evacuation on Sunday we did the first set of experiments.
       
 (DIR) Post #B6UZQ1ulsikNoKS6Km by dlakelan@mastodon.sdf.org
       0 likes, 0 repeats
       
       @IzzyOnDroid Subscribed to your Liberapay for $36/yr thanks for your work!