Formal verification at the undergraduate level, if you even see it, would be about running software on a spherical cow, though.

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.

CodeWeavers, AIUI, have a plan - and their plan may also be using FEX as a basis.

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!)

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.

"You can't" should be the ONLY acceptable answer.

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.

(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?)

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.)

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.

- 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.

An example: a vector of things to a thing of a vector, for "thing" in (promise, option, result, ...). 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.