codebje

If it can give me the recipe without 14 pages of backstory about how Nonna used to make it, it'd be satisfying a real need.

Formal verification should definitely be about the software you're verifying exhibiting the properties you desire under the conditions you specify.

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

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.

How different is this to, eg, the Google developer program, in which I can create a new OAuth client for Google users?

There's lots of things to show for the research!

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.

They're using a custom fork of FEX (https://fex-emu.com/).

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

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.

They were not keeping it beyond the timeframe necessary for the model to process it, so there wasn't access there to audit.

Same reason you wouldn't just emulate a Z80 on a desktop. People don't build retros because they're practical.

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?

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

Authorisation is a way to do that, too.

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.

Sounds like an argument for organised labour to me!

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.

The context window limit prevents it, for one.

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.

Here's some reasons:

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

You can use a similar design to your existing fleet without a literal retrofit of an existing chassis to shoehorn a battery and electric drive train in there.

The retrofits usually are less preferable not only because of pointless inconveniences like transmission tunnels, but because they'll be the manufacturer's first toe dipped into the EV waters. The retrofit chassis speaks to either a rush to market, or a cautious approach not wanting to commit too many resources. The former says it'll have issues, the latter says they might bail on it and leave you stranded for service and repairs. Or both at once.

The malice is by the author of the malicious skill file.

This is an intrinsic risk associated with giving LLMs access to sensitive material. It's reckless of Microsoft to give an LLM such broad access based on the user's own permissions.

If there were a confirmation prompt for the Teams message, why would even a highly competent user refuse it? That's what the skill says it will do. The message is expected, the visible content is expected, a confirmation prompt is just a nuisance.

I don't think it's a new normal. In my experience a large volume of text rarely has a lot of information to convey. Instead, it's intended to convey the sense that a lot of work has been done.

The consultant mindset set this trend before AI made it all worse.

Without passing opinion on GP's point, I think that just proves it's hard to establish a data set that doesn't bias toward the result you're hoping to find.

I think that it feels a little wasteful to go to Google search to ask a question like this, only for the AI that's giving you an answer instead of page results to perform its own web search to get you the response.

Also, I asked a thinking model with browsing enabled and got this:

The Google Pixel 10 is expected to support Wi-Fi 7 (802.11be), based on the Qualcomm Snapdragon 8 Gen 4 / Tensor G5 chipset it will likely use, which includes an integrated Wi-Fi 7 modem. Specific finalized specs aren't confirmed until Google's official announcement.

(Model GLM-5-Turbo - two months old - using Kilo Code in the "Ask" profile; in its thinking token churn it reasoned that it should keep the response brief and direct. Perhaps not the best suite of model+harness for this task, but it's what I had to hand that's not quantized to shit, is a thinking model, and has a web search tool available to it.)

I am fortunate enough to have both a butterfly keyboard MBP and a touch bar MBP. Obviously the butterfly keyboard has the known issues, but the touch bar MBP also has the very common issues with that hardware.

I can replace the butterfly keycaps myself. It's something like $10 from aliexpress for a full set of keycaps and clips and a minute's work to pop the busted one and replace it. Annoying, but not fatal.

The touch bar needs a full battery, keyboard, track pad, and upper case replacement to fix. I just have to live that that thing flickering brightly at me every day, or spend AU$500+ to get it fixed.

IMO the touch bar is the bigger mistake.

Because LLMs aren't sentient, they don't draw on facts, and they don't have nuance. The answer given is similar to answers you might expect to see for similar questions.

It's really amazing we can make machines do that, and it's really depressing that we think a stochastic bullshit machine is going to give us something we can rely on.

If you have an interpreted language, you don't have a C function corresponding to each language function. You have a C interpreter loop with a "current instruction" pointer. When the current interpreted instruction is a call, you check all the things you need to check, push the current IP to a stack, and set the IP to the first instruction of the function.

C's type checker never sees the interpreted language's functions.

Thanks for the response. I really like the measured, evidence-based approach you're taking to this work.

I have the wrong CPU architectures for pre-built jank packages (x86 mac, aarch64 linux, the exact opposite of 'normal') so I haven't actually looked at what it produces, so my last paragraph was pure speculation. I appreciate the detail you gave!