I've loved the idea of a computer on my wrist since I was a kid but now they're available, I find myself unable to think of an actual useful application for them apart from telling the time - what do you smart watch people actually do with them? Are they mainly toys or do they enrich your life in some practical way?
Biometrics, heart rate and sleep tracking are huge, like 95% of the reason I own a smart watch. It's a sensor, not a UI. Everything else can be done better on a phone.
I turn off notifications (because if I get a message on my watch, what am I going to do with it? watch is basically read-only)
One use that comes up a lot: setting a timer. Being able to ad hoc set timers with your voice is huge - without it, my coffee would get cold, my laundry would stay wet, and my kid would be late because dad got distracted by a HN comment.
1. Notifications. Most useful in noisy environments such as grocery stores, airports, shop floors, or any place you may be wearing hearing protection. Also great while working with your hands, like car work or cooking and directions while driving. It’s best to limit them to the apps that matter, and only when you need them.
2. Biometrics.
However, after this watch finally dies, I don’t think I will be going back. Big reason is smart watches are not stylish at all. For men watches are our only fashion accessory that we can freely wear in all occasions. No matter what band or watch face you use you are stuck with a black square attached to your wrist. Also smart watch battery life is a bit of a bummer, it’s hard to beat self winding or solar powered watches that you never think about changing as long as you wear them.
Yeah the battery life is off-putting for me - watches I had as a kid would last for years on a single battery so I think I have that expectation stuck in my mind. I do like the biometrics angle - something that tracked my health condition and alerted me to any problems would be interesting, but it would have to be fully under my control; I'm not keen on my health data disappearing into who knows what databae.
There are reportedly solar smart watches. I do wish my dumb watch was a tad smarter in that it doesn't get automatic time updates, but that's not impossible even without a phone. I haven't found one that's waterproof, solar, wireless time, and the right price though.
It helps mine runs a bit fast so I'm early to things. If it ran slow I'd probably have replaced it years ago. As is, I'm going on 10 years with barely taking it off my wrist and never charging or replacing a battery, and I'm not the first owner.
Citizen has an Atomic Timekeeping Eco-Drive series of watches that have a 200 meter water resistance. If you like complications see the Promaster Skyhawk A-T.
Sadly I got my current watch for free and it still works. And I don't really get dressed up for stuff. So while yes they certainly do have a series of nice looking watches, I can't justify the purchase at the moment.
They're great for doing phone stuff without pulling your phone out of your pocket and unlocking it. I can check if a notification is important, get GPS directions, snooze alarms, get OTP/2FA codes, or check the weather. None of it it is critical but it's collectively a quality of life improvement.
I stopped wearing my Apple Watch because notifications were too distracting when trying to work (even with Work Focus, I want some notifications, but I don’t want my wrist buzzing and lighting up all the time). I don’t miss it. The only real use I ever got was GPS directions when riding a bike or electronic scooter. I guess I also tracked my runs with it. But I don’t use those often enough, and I can wear the watch for those situations if needed.
I do also love the idea, though. I think part of the limiting factor is that you can’t attach sensors or peripherals to it. Even with a hackable watch like in TFA, there’s only so much you could add without it getting bulky. And the screen is too small to do much with.
I switched from Apple Watch to a Garmin Fenix 7, for much longer battery life (advertised as ~14 days, in practice 10-12), durability (they're very tough), better biometrics, and stuff like built-in maps/GPS (I camp/hike/hunt/etc a lot). I just didn't use any watchOS features, and I use an MVNO that doesn't support sim cloning so cellular's a wash. In short even with reduced features I am considering just going back to an old analog Timex Explorer and using a dedicated GPS device, because even the more limited feature set of the Garmin seems like I'm barely using what it's capable of.
Don’t have one capable of it, but listening to music whilst running without a clumsy phone to hold/strap to my arm/put in a silly belt would be awesome.
As a former user of the Sansa Clip, I recommended the Shanling M0 as a modern alternative (they sell a separate case for the clip if you want that). Great audio quality and features, format and Bluetooth codes support.
Same here, loved the idea since I was a kid and I spend a lot more money on gadgets than I probably should but somehow managed to avoid getting a smartwatch because it doesn’t do anything a smartphone does better. I just wear a simple casio solar powered watch I got for about $100 which I never have to charge. I still like the idea of something programmable though, but this watch in OP is a bit too DIY for my tastes.
Smart watches, in general, have a better GPS antenna. I tried running using just my phone's GPS and it's all over the place, completely unusable for that task (it showed me crossing walls, canals, running in circles where I went in a straight line etc.)
Also, a lot of smart watches come with a pulseox, so, you can look up your pulse any time you like :D Not super useful unless you are working out, but there's that.
Some applications that we use in smartphones are very useful, like the alarm clock. I have begrudgingly adapted to their quirks and privacy implications. I'd rather program my own versions, same for smartwatches.
Alarms I can understand, but that's been a feature of standard watches almost since they were invented I think. I'm looking for something that requires a programmable device to be meaningful and so far the ideas are fairly thin on the ground :-) I get the techy appeal though, and agree wholeheartedly about the value of having total control over a device if possible.
I run every day. Started doing it for multiple reasons, some of them being health. The watch tells me my pulse, speed, cadence, calories burned. I doubt the numbers are very accurate, but they are consistent, and, probably, not too far off outside of cases of obvious misreading. It also has a way of collecting some data about swimming (which I don't understand, like what is swolf? I know, I could look it up, but I'm a terrible swimmer, so I don't bother).
For people who like to leave their phone in random places around the house, the watch can help in locating it. You can also almost always turn off the alarm on your phone w/o getting out of bed (provided you sleep with your watch on and the phone's bluetooth didn't decide to randomly disconnect).
All this said, I think that smartphones, in general, provide very marginal utility. A little bit of convenience here and there but nothing groundbreaking. If phones had better GPS antennas and a framework to attach devices like pulseox or sphygmomanometer they'd be preferable to the watch because the display is bigger and the input is (slightly) more convenient.
Yeah fitness tracker is a good one; I'm the opposite with my phone though - I get a ton of utility out of mine, but not things that I think would be improved by shrinking them down onto my wrist.
Nearly 50% of US voters voted for the current administration last time - do you think all of them are on board with the Iran war? There are multiple reasons for a person to vote for a political party; China is a big issue in Taiwan but it's not the only issue.
The kind of reaction described by the GP is probably trained by a lifetime of bad experiences. One can end up going into every interaction thinking about which parts of oneself to dial down in order to have some semblance of a normal conversation, and inevitably that over-thinking just makes it worse. Ask leading questions, smile, listen careful, don't interrupt - you know, all that sort of thing that comes more naturally to some than to others.
> going into every interaction thinking about which parts of oneself to dial down
what if (a) I hate leading questions, (b) by default only smile when bad/tragic things happen (eg "train crash leaves 100 dead and maimed"), (c) I'm quite bad at listening bc if you don't say interesting things often/densely enough my mind adhd-s away, and (d) interrupting is second-nature to me?
...advice may be good, but for some of us it's like 99% of ourselves that we need to dial down in order to carry on a successful interaction - it works, but takes a hell lot of energy
You seem to have a lot of limiting thoughts about yourself. Other people do those kinds of things but just don’t mind and don’t think that they are a bother to others.
You’re allowed to be weird. Weird people make the best conversation because you don’t know where they’re gonna go
Yes, you and I are making the same point :-) There's lots of useful advice out there about how to be a better conversationalist but it's exhausting for those of us who have to constantly think about it, and disheartening when we get it wrong despite all the effort.
For example using nested .gitignore files vs using one root .gitignore file. I guess this principle is related to this one:
Imagine the code as a graph with nodes and edges. The nodes should be grouped in a way that when you display the graph with grouped nodes, you see few edges between groups. Removing a group means that you need to cut maybe 3 edges, not 30. I.e. you don't want something where every component has a line to every other component.
Also when working on a feature - modifying / adding / removing, ideally you want to only look at an isolated group, with minimal links to the rest of the code.
You're describing "modularity" or "loose coupling" in code. But it rarely implies you can just delete files or directory. It usually just means that a change in one component requires minimal changes to other components -- i.e. the diff is kept small.
Are you on some point-release distro that never pulls in the latest frameworks? I know I've noticed a big uplift in stability by using a rolling release base, or Flatpak if stuck on "stable".
Privacy friendly version of Last.fm for those that want to see a history of the things they've played.
I have a history that goes back almost 10 years at this point on a self hosted service.
I used to use last.fm, I switched to MusicBrainz last year. It has much better API access and I have a history of songs I've listened to since I was 17 in 2007. It's a time capsule, a tracker, a playlist generator and a record all-in-one. Scrobbling is just a word meaning 'to track listens'.
You can use it to generate recommendations in MusicBrainz for discovering new music.
I use it just because I like exploring how my tastes change over time.
We're not speaking about bugs in a verified system so much as writing articles making specific claims about that. Surely if we're at the level of precision of formal verification, it's incumbent upon us to be precise about the nature of a problem with it, no? "Lean proved this program correct and then I found a bug" heavily implies a flaw in the proof, not a flaw in the runtime (which to my mind would also be a compelling statement, for the reasons you describe).
Or it implies a bug in the specification. The spec differing from the intent is a frequent source of bugs, it doesn't matter what language the spec is written in. Most people have experience with (or have seen news stories about) specification bugs in natural-language specifications: legal loopholes!
This is the biggest risk with the rejuvenated interest in formal proof. That LLMs can generate proofs is useful. Proof assistants that can check them (Lean/FStar/Isabelle/...) similarly so.
But it just moves the question to whether the theorems covered in the proof are sufficient. Underlying it all is a simple question:
Does the system meet its intended purpose?
To which the next question is:
What is the intended purpose?
Describing that is the holy grail of requirements specification. Natural language, behaviour-driven development, test-driven development and a host of other approaches attempt to bridge the gap between implicit purpose and explicit specification. Proof assistants are another tool in that box.
It's also one of the key motivators for iterative development: putting software in front of users (or their proxies) is still the primary means of validation for a large class of systems.
None of which is implied criticism of any of those approaches. Equally, none completely solves the problem. There is a risk that formal proofs, combined with proof assistants, are trumpeted as "the way" to mitigate the risk that LLM-developed apps don't perform as intended.
They might help. They can show that code is correct with respect to some specification, and that the specification is self-consistent. They cannot prove that the specification is complete with regards its intended purpose.
Sorry, I'm not sure I follow. We are talking about bugs in a verified system, that is, in this case, a verified implementation of a zlib-based compression tool. Did it have bugs? yes. Several in fact. I'd recommend reading the article for a detailed listing of the bugs in the tool.
> The most substantial finding was a heap buffer overflow! but, not in lean-zip's code, but in the Lean runtime itself. (emphasis mine)
> The OOM denial-of-service is straightforward: the archive parser was never verified. (me again)
"Lean proved this program correct" vs "I found bugs in the parts that Lean didn't prove was correct". The failure was not in Lean's proof (which as I said is heavily implied by the title), but in ancillary or unverified code.
Do I misunderstand how Lean works? I am by no means an expert (or even an amateur) on Lean or formal systems in general. Surely the first class of bug could be found in any code that uses the framework, and the second class of bug could happen to any system that isn't proven? Does that make sense? Otherwise where's the boundary? If you find a bug in the OS, does that mean Lean failed somehow? How about the hardware? If your definition of a 'formally verified system' goes beyond the code being verified and the most important thing is whether or not you can make it crash, then the OS and the hardware are also part of the system.
Of course bugs are important to users regardless of the cause, but the audience for your article seems to be software engineers and as a software engineer, your article was interesting and you found something useful, but the title was misleading; that's all I'm saying.
Further to my earlier reply - a more succinct way to look at it might be:
- When they fix the run time, bug A goes away. So the proof still holds and the zlib code is still correct.
- When they add a system of proofs for the parser and modify that, then bug B goes away. So the proof still holds and the zlib code is still correct; and now more of the library is proven correct.
The formulation of the title is "I was told X but that's not true"... but that's not true. You were told X, and X is true, but you found Y and Z which are also important.
There are two different answers to this question, and which one is "correct" depends entirely on the context of who is asking it.
1. It's the code that is specific to this program that sits above the run-time layer (internal view, that most programmers would take).
2. It's the code in the binary that is executed (external view, that most users would take).
The key question does not seem to be "was the proof correct", rather "did the proof cover everything in the program". The answer depends on whether you are looking at it from the perspective of a programmer, or a user. Given the overly strong framing that the article is responding to - highlighting the difference in this way does seem to be useful. The title is correct from the perspective that most users would take.
Yes but, without wishing to be snarky, did you read the article? There is no program as such, in either sense - the announcement from Lean only mentions "a C compression library" (zlib). Not only that, but since we're talking about formal verification, a programmer would likely understand that that is about proving a bounded, specific codebase at source code level, and not operating on a binary along with its associated dependencies (again caveat my limited understanding of these things).
My feeling is that if you told the average non-technical user that some person/organisation had produced a formally verified version of a C compression library, you would likely get a blank look, so I think it's reasonable to assume that both Lean's intended audience, and the audience of the blog post linked here, correspond with number 1. in your list.
The article describes fuzzing the library, this execution requires a program to be compiled. Typically fuzzing involves a minimal harness around the payload (a single call into the library in this case). There is clearly a bug in this program, and it does not exist in the minimal harness. It must be in the library code, which was covered by the proof.
The bounded, specific codebase that you refer to is typically the library *and all of its dependencies*, which in this case includes the Lean runtime. This is why formal verification is difficult: the proof chain needs to extend all the way down to the foundations. In this case the original gushing claim that everything was verified is incorrect and premature. The article seems like a good exposition of why.
Thank you, I understand what fuzzing is; that test harness was presumably provided either by the blog post author or generated by Claude somehow, and therefore would not have been part of the proven code, nor part of the original claim by the Lean devs. That's what I meant by saying there is no program as such.
> The bounded, specific codebase that you refer to is typically the library and all of its dependencies, which in this case includes the Lean runtime.
How does that work? I thought the main idea is to write code in the Lean language which has some specific shape conducive to mathematical analysis, along with mathematical proofs that operate on that code. How then does a system like this handle a third party dependency? I've searched around and I can't find any information about how it works. I assumed that the boundary of the proof was the source code - surely they can't also be proving things like, say, DirectX?
> This is why formal verification is difficult: the proof chain needs to extend all the way down to the foundations.
The difficulty is not in explosions of computational complexity due to problems of incompleteness, decidability, the halting problem, those kinds of things? As I said this is not something I know much about but it's surprising to me if 'analysing all the code' is really the difficult bit.
There are standard convex assumptions to handle incompleteness, decidability etc, i.e. the results are an over-approximation that terminates. Picking a approximation that is precise enough in the properties that you care about is part of the challenge, but it is an in-band problem. There are no hard edges between the theory and reality.
As with most engineering problems the out-of-band issues tend to be the hardest to solve. Models of the part underneath the interesting part need to be complete/accurate enough to make the results useful. Compare it to crypto where people do not usually try to break the scheme - they try to break the specific implementation of the scheme because the weakest points will be at the interface between the theoretical construction and the actual concrete instantiation of the device that it will run on.
I am pretty sure you could tell a teenager "there's a ZIP compression program that's scientifically proven to have no bugs" and they'd understand you. People don't have to be CS experts to understand that. (Technically it's Gzip but that's mostly irrelevant to understanding the claim here)
Gentle reminder about this excerpt from HN Guidelines:
> Please don't comment on whether someone read an article. "Did you even read the article? It mentions that" can be shortened to "The article mentions that".
Say you study some piece of software. And it happens that it has an automated suite of tests. And it happens that some files aren't covered by the test suite. And you happen to find a bug in one of those files that were not covered.
Would you publish a blog post titled "the XXX test suite proved there was no bug. And then I found one"?
These were my thoughts as well and it's nothing new, I think, regarding testing altogether:
- testing libraries (and in this case - language itself) can have bugs
- what is not covered by tests can have bugs
Additionally would add that tests verify the assumptions of coder, not expectations of the business.
To give benefit to the author - I'd read the article as: having tests for given thing ensures that it does the thing that you built the tests for. This doesn't mean that your application is free of bugs (unless you have 100% coverage, can control entire state of the system, etc) nor that it does the right thing (or that it does the thing the right way)
I like to differentiate between coverage by lines and semantic coverage: sometimes you need to exercise a single line multiple times to get full semantic coverage, and better semantic coverage usually beats larger line coverage for detecting problems and preventing regressions.
Yes, mutation testing and similar techniques like fuzzing can help with it, but sometimes you want to be more deterministic: there are usually a lot of hidden side effects that are not obvious, and probably a source of majority of software bugs today.
Eg. something as simple as
function foo(url) {
data = fetch(url);
return data;
}
has a bunch of exceptions that can happen in fetch() not covered with your tests, yet you can get 100% line coverage with a single deterministic happy path test.
Basically, any non-functional side-effect behavior is a source of semantic "hiding" when measuring test coverage by lines being executed, and there is usually a lot of it (logging is another common source of side-effects not tested well). Some languages can handle this better with their typing approaches, but ultimately, there will be things that can behave differently depending on external circumstances (even bit flips, OOMs, full disk...) that were not planned for and do not flow from the code itself.
You're technically right, but what things are versus how they're promoted or understood by most people (rightfully or not) often diverges, and therefore such "grounding" articles are useful, even if the wording addresses the perceived rather than the factual reality.
By way of analogy, if there was an article saying "I bought a 1Tb drive and it only came with 0.91 terabits", I think if you started explaining that technically the problem is the confusion between SI vs binary units and the title should really be "I bought a 0.91 terabit drive and was disappointed it didn't have more capacity", technically you'd be right, but people would rightfully eyeroll at you.
To be clear, I think the article was fine and the author did some useful work (finding a bug in the runtime of a supposedly provably correct system is indeed a valuable contribution!). I don't agree that it's pedantic to explain why the title feels like a bait-and-switch (and thus does a disservice to the article itself). It's just a bit of feedback for future reference.
I take some comfort from being technically correct though; it's widely accepted by all of us pedants that that is the best kind of correct ;-)
No, it's much better for the business magnates if you spend all your short lifespan on solving problems every waking hour. Don't worry about experiencing your life, you need to generate value!
reply