For one, I have strict iptable rules to drop inbound from outside my specific commercial subnet and my specific residential IP. After that, all the usual best practices.
I also don't think there's been nearly enough time for peer review of what was actually formalized vs what was intended. How many humans out there actually have a deep enough understanding of the background to be able to check the work? I understand that Lean checks the mechanical steps, but if it's building a ladder to some other result entirely, nobody (certainly nobody on HN) will know for some time.
I'm probably wrong, but what's the point of throwing away all skepticism?
Oh I fully understand how Lean works, how minimal the kernel is etc. I just think that just because "it compiled", we don't actually know that the autoformalization proved all the right stuff along the way. After all, LLMs can produce correct proofs for statements that don't align with the original intended theorem [1]. I just think we should be a bit more skeptical in general before saying these seminal results are fully true. What's the rush?
I just think that with the vast amounts of compute involved and the tendency to reward hack, we can't assume the steps towards that formalization are without error until full human understanding of the formalization.
I think that on closer inspection, a lot of these fully AI generated proofs will fall apart. Even in Lean, you can build theories which compile but nonetheless state something different than what you actually intend. It's just that the volume of proof is so staggeringly large that it will probably take years before we find the issues, a la abc conjecture
Battery life optimization on Lenovos often involves installing and activating the correct GPU kernel module. My battery life on my P53 improved measurably after doing this, though installing new kernels involved a small build step. Are you just running with all the defaults?
I have an axolotl. They're really incredible creatures, with way more personality and interests than you would expect. They are really soft, and almost have the same density as water, so they can be neutrally buoyant and even swim rapidly like a fish. They're also very sensitive to sharp things; mine recently got a cut from an aquarium decoration, which healed fully over the course of a week. Her previous owner had neglected her and induced tail curl, which took longer to heal (a few months) but did fully heal. I have since adjusted her tank to give it all flat or smooth surfaces, with some variety.
It generates additional code that's fed into an SMT solver. Poor compiler performance is a top issue developers have with Rust, which they're working to solve. I think adding this layer into every piece of code (which is probably impossible since inferring the invariants is essentially inferring your business logic) would eat away gains they've achieved.
I also think the functional style, typestate, and borrow checker is enough for writing correct code across many business domains, so there's no need to add this to your toolchain. We are a med device company building a class III (really 3 class II) device, and Verus is making our verification story extremely compelling.
I'd rather have all the unsafe code scoped and the safety invariants explained than the alternative. You still can't do a whole class of scary things in an unsafe block; common misconception
The latest CGMs are definitely not cheap on the R&D side. The obvious implementation is really susceptible to interference from common drugs, which is a really expensive thing to fix. They're also trying to get wider adoption in the hospital which requires fixing similar issues with many different compounds. FDA is still quite tough on biocompatibility. They definitely are taking a good profit though.
I'll be showing my bias here, but you're probably referring to NICE-SUGAR, which I think suffered mainly from having a pretty uninspired control algorithm. We built and simulated it and several other clinical protocols and it had the widest spread of performance, but it lost a ton of points to hypoglycemia performance, which is where you get into increasing mortality. The NICE-SUGAR protocol [1] has no notion of weight based dosing, and even has some completely missed edge cases. There have been similar studies in Japan with a better algorithm and they showed the expected benefits.
Recall that GLP-1s were originally designed as next-generation long acting insulin modulators; they're a form of passive control. The CGM gives you data to act on, or at the very least observe. I find, from my experience wearing them as a person without diabetes, they give really interesting insights into my own life by giving numbers to stressful moments, which can be good insight to have. That's called stress induced hyperglycemia. Everyone has a unique and continuously evolving glucose system, so YMMV.
Drug interference (with the sensor chemistry) and perfusion (which the sensor needs to function) are two major problems that a hospital presents that are not present in ambulatory (outside the hospital) use. Also the FDA has not approved any systems yet; the software is actually quite difficult to get right.
If the large studies are to be believed, you could save hundreds of thousands of lives and many billions in excess expenditure, because stable blood glucose shortens length of stay. People with diabetes alone account for 60% of hospital expenditure, so improving their care improves the system in a big way.
I've had the fortune to work with several CGM OEMs behind the scenes as part of our work developing an artificial pancreas, they all have a secret lactate signal!
Lactate's available in the internal engineering data of these sensors, just not something that anyone has wanted to spend the time or money to qualify with the FDA. It essentially comes "for free" due to the chemical reaction the sensor uses.
It can happen in people with uncontrolled T2D as well. My cofounder is a pediatric ICU doctor who has treated hundreds of DKA patients.
Also there wasn't really a relationship of the keto diet to the rest of my post, just using it to contextualize a technical term with one that might be more familiar.