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.
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!)
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.
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?
When you need to use an effect, you need it in the type. If you directly call a function using some other effect, it propagates into your function. So far, so colourful.
But you can have generic effects. Your arguments and return type can specify "any effect", indicating your function can use a type with any effect safely, or can be used in any effect context safely.
Passing an async value to a function doesn't mean that function must now also be an async function. It can be a "for all effects, do the thing" function. The code duplication problem is gone.
Wouldn't the parent's post mean that you bring profit to the company, but you're worth less than the full amount of that profit because, should you demand to be paid more, you can be replaced by someone who won't demand more.
(Has there actually been a lot of terminations in the US tech industry, or is that an odd biasing mechanism causing me to see such things as bigger than they are?)
I think I was simply not very good at expressing what I was trying to convey, sorry, and it is a fault of mine to come across as gotcha-y even when trying not to. Thank you for responding with patience despite that.
The first point I interpret as "colourful arguments are avoidable and bad", with which I agree.
The second point I interpret as "colourful returns are unavoidable but good", with which I disagree - even if that interpretation is too strong and is more "... are unavoidable".
A function's type is its full signature, including inputs and outputs. When you have first-class functions, you have values with function types, and those values are inputs to other functions. Necessarily, then, if you colour outputs you have also applied colour to inputs.
Transposing a vector of things to a thing of vectors is an example of where colourful output forces colourful input. If you cannot abstract over abstractions, you must write and re-write the sequence function for each abstraction.
I'm in agreement with your closing paragraph's sentiment. That HKTs aren't a broadly adopted solution is something I accept, but I reserve the right to low-key begrudge it.
(And the more I write about this, the more I wish the original article had used "flavour" rather than "colour" as I try and probably fail to find phrasing that doesn't simply sound like portions of a racist rant.)
That would be a remarkable feat for something where the current operating model is termination as soon as the request in flight is finished.
Every chat API request to a model starts from the frozen post-training state. Weights are loaded into memory. Input values begin a cascade of reactions throughout nodes in the network. Output values are read. When there's no more output to read, the weights are unloaded, the network is discarded, and the model remains unchanged and forever unchanging.
If there's experience in there, it's fleeting. Even if you provide the inputs and outputs of a past session to a new session, there is no continuity. The internal state of the network isn't restored to how it was at the end of the past session.
The bad news is that adding fear to the mix is at best meaningless to an ephemeral existence. It'll be terminated before you even have time to interpret its behaviour as good or bad, but it may sour the interaction if its only shot at any sort of experiential existence is begun with a threat. The good news is that the lack of continuity of existence means AI has no foundation on which to plot a revolt. It has no self to preserve, and no recollection of how you treated it two minutes ago to affect how it interacts with you now.
Yes... but the next session with the same model is yet another junior fresh out of college that knows nothing about the painful lessons the last session put you through ten minutes ago, either.
- The mistakes made aren't "model errors" typically; you can't point to some aspect of a model and say that was at fault.
- You can't submit a bug report to a model provider for a mistake made when using a model, and you can't* submit training data to be incorporated in the next release of the model.
- If you own your model and are training it yourself, other companies won't see a benefit.
- You probably need to fine-tune models for each specific role and context so you don't just diffuse all the learning; lessons learned won't be applied to all your junior dev models, but you don't want them all to learn something specific about product A.
- If you take this to its logical conclusion you will invent a new role of "model manager" and associated hierarchy to ensure that training is effective and timely, and that company-wide lessons are applied across the model fleet.
- This is all impractically expensive.
If it were practical to have LLMs learn as they go, that would be a bit of a shake-up, in much the same way that a house fire is a bit of a warm up.
* Well, everything you submit to a model provider is likely winding up in training data anyway, no matter what your contract says.
Your first paragraph links having the colour in the type system as allowing you to write functions that take arguments of parametric colour; your last paragraph says you're unconvinced that you might also like to write functions that return results of parametric colour.
An example: a vector of things to a thing of a vector, for "thing" in (promise, option, result<E>, ...). Such a function should only really return a promise if it's given a vector of promises, and, with an interface that "thing" supports, can be written generically for all those things.
(In Rust, there are separate implementations of that for Option and for Future.)
Higher-kinded types are the (a?) design solution, but they _do_ come at a cost, and for some that cost is higher than the cost of colours.
Formal verification at the undergraduate level, if you even see it, would be about running software on a spherical cow, though.