Well, ideally you proof should've failed because your axioms should be aware that arithmetic operators in the programming language of your choice are operating modulo some large power of two, and thus don't produce correct results for some particular inputs.
Admittedly, this one peeves a lot. Remember when Java's binary search and mergesort (and implementations in many other languages' standard libraries) turned out to have a bug of this kind [0]? Admittedly, the proof was informal, but if you are trying to prove some properties of a program X written in a certain programming language Y, you can't "just assume" that the semantics of Y are different from what they are, right? The integers do overflow in Java, that's explicitly stated in the Java's spec... and that means that a lot of even the most simplistic code has some very non-obvious correctness preconditions, which most of the times, I believe, are simply hoped to be true.
I am not sure that the perspective you have taken is the same as what I understood from the parent post; what I took from it is that things like registers, memory locations, ways to implement square root, and so on, are all _implementation choices_ that are not important properties of the specification. You specify that the hypotenuse is the square root of the sum of squares, but whether square root is implemented using Newtonian approximation or a fast inverse square root is irrelevant; whether your first argument is passed in a register or on the stack is irrelevant.
Often, things like resource usage are not specified: running time, memory consumption, etc, aren't relevant enough to appear in a behavioural specification.
If your spec says "f(a, b) returns a + b", but it's just a high-level document you can use to help guide your implementation, integer overflow is just one of many ways your implementation might be inconsistent with the specification. It's still likely that the existence of a formal specification you reference during implementation means that more edge cases have been considered ahead of time than if you just had an informal spec.
If, on the other hand, you prove it but it turns out not to be true (ie, you overflow integers), your proof is wrong. If a machine verified your proof and gave you a big thumbs up, your machine verification is wrong.
If, in Idris, I write "f : (a : Nat) -> (b : Nat) -> (c : Nat * c = a + b)", then I cannot compile an implementation for which I can't show a proof that the result is _always_ the addition of a and b, for all a and b, unbounded by anything but the resources at hand with which to run the program. An implementation subject to integer overflow won't compile.
Or, I could write "f : (a : Bits32) -> (b : Bits32) -> (c : Bits32 * c = a + b)" and implement something where , but then modulo arithmetic on overflow is _part of the specification_, because "+" in there is doing the heavy lifting of being defined as addition modulo 2*32 already; by specification, 4 billion plus 4 billion is ~3.7 billion.
Everything the parent comment mentioned were implementation details that did not affect the correctness of the code.
I just wanted to point out that there are implementation details that DO affect the correctness of the code.
And, of course programs need to run on multiple architectures. So it's hard to do what people seemed to be talking about in this thread and verify code just from the source code.
If you have the luxury of proving the correctness of the CPU, compiler and OS, that should be a big win. Otherwise, it seems to just be another type of testing. Still useful, but calling it verified or proven seems a bit much.
From my perspective, it seems more to be writing another, more complicated program, with more opportunities for bugs, and seeing if the results agree
Thank you for your feedback - I have it working on iPadOS 26.5 (Chrome and Safari). The browser auto-play policy does require some interaction with the page before it will play (so the first key press is often mute, but should sound after). There is a button on the control bar to enable sound explicitly. I will look for more instances (not to ask the really obvious question, but do you have sound turned up or a bluetooth connection you're not aware of by any chance?). Thanks again
The coding isn't the hard part. It's the people and networking. Facebook's only moat is HOA boards that think private communication behind Facebook groups somehow equates to public messaging a community...
In other words, once people got on it, it was too late.
The company doesn't have to go away, the app just has to have issues. At least with web apps, you aren't depending on the manufacturer investing in nearly continuous upgrades to work in the rapidly changing phone environment
A web UI will continue to work for decades. And app will likely not last a year without updates.
They basically are. They just license their name out now, it’s like buying a Kodak router.
(That’s actually relatively common with various tech-adjacent companies, e.g. off the top of my head both Energizer and Philips license out their brand to third parties for random crap, even though they make actual products themselves too.)
Really. Because it looks less useful than its source.
If I search for Apple on food central, I get offered different types of Apple, like Fuji, honeycrisp, etc. with nutripedia I just get raw and cooked, which are within each type on food central.
In addition, nutripedia has a bunch of what looks like AI written text that is not particularly useful.
Writing an AI generated wrapper around something is not enough to be interesting. What do you see as your value add?
Like a time capsule. Last modified date at the bottom of the page says 2007.
Also:
> Saffron has been licensed to Adobe and is shipping in all Flash-based products, including Adobe Flash CS3. The Adobe Flash Player is the world's most pervasive software platform and reaches 99% of Internet-enabled desktops.
I might be better off getting something with a beefy GPU on AWS or Google cloud.
reply