codebje

CP/M-86 was definitely a thing, but CP/M-386 was not. By the time the 386 existed, DRI had dropped the CP/M name in favour of Concurrent DOS - though they had MS-DOS compatibility in Concurrent CP/M - and, as you say, eventually renamed it to DR-DOS.

Much as I loved DR-DOS, it did have occasional compatibility hiccups.

Can you expand on your understanding of GRIN doing parts of supercompilation? As I understand it, GRIN doesn't do any supercompilation; it's a structural transformation optimiser built for functional languages, analyzing program flow across function calls for the whole program at once.

As I understand supercompilation, it's an extension of partial evaluation - optimisation is done on a graph of possible execution traces. The downsides should be obvious: execution traces rapidly grow massive, compilation resources grow superlinearly, and there are many cases in which the result is worse than the original.

What value would Fuse get from equivalence of terms, do you think?

It's nice to see a GRIN backend in the wild!

It looks like a tidy little functional language - a small, easily grasped syntax surface and generally clear semantics. That you've got it to the point that it can compile and run proper programs is a great achievement for a solo dev project!

The string type in the standard library isn't Unicode-aware, might be worth just noting that. Unicode support can be a big undertaking, but considering whether you'll add it later or not might affect your library design now.

I don't really understand why you have an IO monad. The language isn't pure - `.exec()` means any function can perform IO actions no matter its type signature - so what's IO really for?

Do `impl` additions export? What happens when two libraries add the same function name with different signatures (or just bodies!) to a type's `impl` ?

Is currying automatic? It doesn't seem to be, but, eg, the `sum(x: i32, y: i32)` function theoretically could be called as `sum(5)` to create a closure, but this isn't a documented feature if so.

The website's font is using ligatures, not unicode operator symbols - I'd personally find it much clearer to use a non-ligature font to show what's really there, but that's immaterial to the language.

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.

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