IMO the biggest issue was always not knowing what correct is in the first place. The vast majority of software we use, the stuff that's riddled with errors, has those errors largely because what it's supposed to do is vague and never, ever deals with edge cases. You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions.
Perhaps that's the same thing as what you're saying, though: we don't specify these things in detail because it's expensive to spend that much time thinking through it all, when users are largely trained to just accept crashes, glitches, inconsistencies, and the occasional sprinkle of data loss.
> . You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions. [..] it's expensive to spend that much time thinking through it all, when users are largely trained to just accept crashes, glitches, inconsistencies, and the occasional sprinkle of data loss.
Indeed. The last bug I fixed in a production app was one where people could not restore from backup due to a de/serialization issue. The correct behavior would have been straightforward to specify (round-tripping). Trying to verify the serializer against the correct behavior would have forced the devs to think through all the edge cases.
> You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions.
This is why it's so important to separate functional from stateful code. Functional code is generally easier to specify. And, by isolating stateful code, one can e.g. fail fast and avoid stepping into undefined behavior.
You shouldn't have been able to formally verify the algorithm fails to protect the critical section. Wrapping ticket numbers can lead to starvation (literally, if we follow the baker analogy), but the algorithm protects the critical section so long as thread IDs are unique.
The sort of environments in which this is a problem would be extremely uncommon. For a start, you need continuous contention. If you ever get a break in contention you no longer have starvation, and you 'reset' the ticket number monotonicity - to zero, if you actually take a maximum of entering thread ticket numbers instead of a cheap global counter.
If you do actually have an environment in which you expect to have continuous contention over a critical section, some quick napkin math can tell you if it's something to worry about based on the running time of your critical section. If it's over, say, 10ms, you've got a few years of runtime before it's a problem. If it's under 1ms, maybe you want to use 64-bit arithmetic for your ticket number so you can run your system until long after the human species is extinct.
You probably got a 'B' because you didn't give the professor the answer they expected, though, not because of any technical reasons.
I'm quite certain I formally verified that two processes were both able to get into the critical section WITH THE ALGORITHM I WAS VERIFYING, but this was 35 years ago, so details are fuzzy.
Remember that this is long before Wikipedia and even before Google, so I have no idea where I'd have gotten the alleged Baker's algorithm from.
Also you're right that this isn't much of an issue in practice, but that's not what formal verification is about, now is it? :)
OAuth2, to be more precise, is a protocol which can be used both for authentication (verifying the user) and authorization (accessing resources on behalf of that user).
Most people in CIAM (customer identity, individuals owing their account instead of representing a company) only interact with OAuth client for authentication. They do not give access of their google account to some THIRD PARTY COMPANY.
Sure they do. All the time! For example, if you want to use a script in Google Docs these days, you have to go through an oauth flow to give that script's app permission to do certain actions in your Docs.
Part of what the research shows is that correctness-by-proof has a cost in developer effort.
If there really is a vulnerability-apocalypse due to AI, and it's not just a different flavour of AI hype, the cost of having insecure software will rise to the point that the cost of dealing with insecure or incorrect code at time of creation becomes less than the cost of ignoring it until it blows up.
I doubt it'll rise so much that we'll want to face the cost of behaviour proofs for much code at all, but it's quite possible it'll rise enough that we want to do things like prove that indices are in bounds, at compile time, so vector accesses can skip checks without compromising safety.
Minor nit: a steam machine is running Proton. Which is wine, yes, but wine that Valve supports, wine with patches and changes (afaik, most of which get upstreamed to wine). On a Mac you're probably going to use CrossOver to package up wine.
Wine is wine, yes, but CodeWeavers is not Valve. Mac gaming is niche. The budgets involved are incomparable. Expect it to take weeks to months for hotfixes applied in days to Proton to filter through to CrossOver.
(This is my lived experience: HD2 patch 28th April broke wine compatibility, Proton had a hotfix in a day or two, CrossOver had a preview that partially fixed it May 11th and a release that fully fixed it June 9th; it was unplayable from April 28th to June 9th, longer if you count the stuttering issue that it suffered since March.)
The future of gaming on a Mac is also made less certain by the upcoming obsolescence of Rosetta. AFAICT Apple won't just pull it out completely, but they're clearly uninterested in supporting it long term, so over time the experience of trying to get x86 games to run on ARM Macs will worsen.
(I think I'll aim for a DIY PC build in 2027 in the hopes memory prices decline by then, but it's a faint hope!)
You are right of course. But I expect that valve will come up with proton-on-arm with x86 translation very soon (in fact possibly next week-ish when they release the frame).
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
If `left_pad()` calls `send_env_vars()`, how can you add exfiltration to `send_env_vars()` without having to change `left_pad()` to expose the use of the network?
Perhaps that's the same thing as what you're saying, though: we don't specify these things in detail because it's expensive to spend that much time thinking through it all, when users are largely trained to just accept crashes, glitches, inconsistencies, and the occasional sprinkle of data loss.
reply