Take a look at Racket (or Rhombus if allergic to parens). Support for contracts there is stellar and provides everything you mentioned. You can use `define/contract` for inline contracts, or you can attach contracts when exporting names from a module using `contract-out` declaration. Contracts are first-class, can be defined separately and attached wherever you want (importantly, this includes values (structs, classes) as well as functions). There are higher-order contracts that generate new contracts from existing ones. There's support for both static and dynamic metadata for almost all kinds of entities in code (ie. both the syntax and the semantic entity it produces can be annotated with anything). I wouldn't recommend using Racket/Rhombus in production, but it's a great preview of what might become commonplace in a decade or two :)
I've spent years avoiding lisp, I am not about to break that streak now.
All jokes aside, I genuinely think that non-algol syntax is a non-starter. We're too far along now, that it's easier for these features to come to java/rust/typescript/cpp than it is to switch completely to academic langs that have terrible tooling support.
The tooling around S-expression syntaxes is almost necessarily better than others because it's so straightforward, eg, structure-based editing operations. The "problem" with IDE integration for such languages is generally the (lack of) availability of static information, especially due to Racket's expressive arbitrarily-many-phased macro system, but that's a separate axis of language design.
That said, the parent comment explicitly pointed out Rhombus as an alternative to an S-expression syntax within that same community, so maybe you could look into that suggestion instead of being pithy about topics in which you are less well informed.
I suspect the GP might not like Rhombus because it uses indentation (like Python) for code blocks instead of braces (which isn't actually Algol-like; IIRC, Algol mostly used parentheses). In that case, even Pyret wouldn't work for them.
Personally, I'm still (25 years into programming) undecided: does syntax not matter at all, matter only a bit, or is one of a language's most important characteristics? It's incredibly hard to say, at least for me.
See the papers "Soft Contract Verification" and "Soft Contract Verification for Higher-Order Stateful Programs" (Nguyễn et al.) In general, there's a lot of academic work on the topic coming from the Racket community.
In short: yes, some classes of contracts can be statically proven. Not all of them, and it depends on the language's semantics, so it's probably not easy to retrofit into C++. But there's work being done on unifying types and contracts, moving back and forth between static proof and dynamic enforcement, and it's all pretty interesting. Proving contracts statically eliminates runtime overhead; generating contracts from types makes it possible for a gradually typed language to be sound.
The basic idea is that you generate "Verification Conditions"(VCs) by mapping the function onto a Hoare Triple viz. {Pre} Function-Body {Post} and then applying Dijkstra's WP-Calculus mechanically to step backward from the Post to the Pre thus generating a mathematical formula.
The programmer provided contracts are merged into this formula to generate the complete VC which is a logical implication viz; Pre ==> WP(contracts-from-function-body, Post).
This is then handed off to a automated solver which verifies that Post is met when Pre is True in all the paths.
I haven't seen those papers. The general thought seems to be that progress is good enough that a restricted subset of C++ can be proved (which is getting less restricted all the time, though probably never will be everything) and the solvers will be able to detect where they give up: if you want a solver you will have to write the code they can prove and that is an acceptable limitation.
Contracts also allow a solver to say "I can't prove this messy function, but I can at least prove everything around it". Which is to say if we prove the precondition is met, and if we assume the post conditions are met, we can prove everything else despite the messy parts we can't do. This at least lets us know where the messy code is.
PvE vs. AI on maps larger than 10x10 slows down to a crawl after ~40minutes. It's not FPS (which remains perfectly smooth), though: it's the simulation speed, influenced by pathfinding, trajectories of every single projectile, managing construction, managing units' scripted movement, and all the AI decision-making. Plus the performance penalty of using Lua (and its GC) for parts of game logic. Apparently, all of that is crammed into a single thread, and by the time you have 1k units, simulating 1 second of in-game time can take 3-4 seconds (or more, obviously, depending on the CPU; but single-core performance stopped improving drastically at some point). It's been a few years since I last checked, but I'd be surprised if anything beyond 20x20 maps would be playable against the AI, even today. And since it's a matter of codebase architecture, fixing it would require a rewrite (someone in this thread is actually attempting it, which could be fun).
Queuing orders in TA and then in Supreme Commanders was best-in-class. Both single units and structures, and groups of them (selected with an assignable hotkey), could have infinitely long command queues. Patrol mode was useful for both engineers and normal units. SupCom added air- and sea-based transportation corridors. The queues were not broken if you ran out of resources temporarily; they just paused and then resumed when possible. I played TA before StarCraft and after Warcraft 2 - I felt SC to be a huge downgrade in terms of controls, and dropped it almost immediately. SupCom then came close to the absolute peak of RTS for me in terms of controls, physics, and economy management. The problem with all the fan-made successors is that I don't want PvP at all, and they seem to focus on that, while the original TA and SupCom were incredible single-player experiences, too.
This is actually a defensible position. It's not either-or - the "gross chuds" doing things you mention are worrying, too. But providing unrealistically attractive depictions of a human body is also a problem. It's been a problem for ages - all the girls and women who try to compete in beauty with celebrities and models (without a team of specialists supporting them), only to ruin their bodies through anorexia or bulimia, or their minds with depression, deep insecurity, and an inferiority complex, exist and deserve mention. AI(-generated images) is not the reason, but fits "well" into the preexisting social problem, and has a chance of intensifying it on a global scale.
You're lucky, since it probably means you never got hit with serious, high-level LinkedIn-speak. People speaking like this exist: I only had one or two interactions, but I honestly ran for my life and sanity as soon as I could. It's eerie, and both possible interpretations ("this guy speak like this for a reason (I'm not going to like that reason)" and "this guy honestly believes what he's saying (is he mad?)") are frightening. I feel really fortunate to only really encounter them IRL this rarely.
HN is an ad platform - it's just maintaining the old style of providing actual value to bribe users into accepting the occasional ad organically, instead of min-maxing for engagement and providing nothing else.
Mentioning LessWrong and 4chan in the same breath made me chuckle, but it's actually a good summary of the modern Internet: to be ad-free, you need to either care very much, or simply not care at all. The middle of the road has been bought, fenced, and you need to pay (with money or attention) to access it.
> Its quite reasonable to assume a future operating system
Possible, yes. Reasonable to assume? I don't think so.
The issue is that we had that for a decade or two already: people who lived through the era will tell you more, but Smalltalk environments and Lisp Machines already realized this "malleability" to the extreme and... died. We got DOS instead; the rest is (a pretty shameful) history.
Emacs is just about the only artifact (along with Squeak-derived Smalltalk-likes) of the era that still exists and is in popular use. The PC revolution killed interactive, vertically integrated, fully programmable environments. It happened because of hardware limitations of the time, but the consequences are cultural: the LispMachine-like environment simply faded from the collective imagination of programmers who learned programming by writing "resident programs" for DOS in assembly. It didn't happen immediately: DOS was sufficiently open for modification that (if you knew x86 assembly) you could mold it to your preferences, but the hardware wasn't powerful enough to do much with it. As hardware advanced, PC OSes ossified, adding abstraction level after level in both hardware and software. Early Windows was trivial to dissect - I remember WindowBlinds, a set of apps that transformed Win 95/98 into almost anything you wanted. I recently checked, and nothing like that is possible in the recent Windows versions. GNOME on Linux seems to have followed the same trajectory (fortunately, there are still a few other desktop environments there).
So I don't think the "malleable software" is going to return any time soon. We have not only rigid software everywhere - we have 30 years of shared culture of developing and using such rigid tools. With the size of the programmer population, changing that culture in any meaningful way seems very hard. There will be people who rediscover Lisp Machine ideas, there will be a segment of users swearing by Emacs and similar apps, but we'd need a revolution in corporate and educational policies to get anywhere beyond that, I think.
Agreed - the circumstances indeed changed, and the possibility of automatically generating code from a natural language prompt is something we didn't have ever before.
As an Emacs user, I can testify that it's a game-changer. Codex CLI paired with `emacs --batch` is perfectly capable of setting up, developing, and testing just about any kind of extension you'd want. And with packages integrating LLMs into Emacs, you don't even need an external harness - open a buffer, type a prompt, get a useful extension or customization. It really works quite well.
But I stand by my opinion: Emacs is just one piece of software, not completely unknown, but rather niche, all things considered. Almost no other app supports seamless extensibility at Emacs' level (not even web browsers come close, and not by accident - it was a conscious decision to drastically limit what plugins can do).
Most programmers don't feel the need to make their apps easily and deeply extensible. Most users don't feel the need to extend their apps - even simple customization is rare. Most product owners don't want users to have "too much" freedom to change things.
So, while LLMs do give us a realistic path towards making extensible/malleable software attractive to users, almost nobody is taking that path right now. Realizing LLMs' potential in this area requires large parts of both the user and developer populations to recognize the possibilities and then actively pursue them for a few years. For now, it doesn't look like anything like that is happening.
Jev was built using the same architecture Laya's author proposed[1] in March 2025. Laya is an open-source system based on that research from a year ago. Whether Jev is also based on the OP's materials or independently invented is hard to say.
My internet provider in the early 90s maintained a Unix system with pine and lynx; it only allowed access to WWW a few months after we subscribed to their dial-up. I didn't know what to do with that remote system, but I knew `cd` and `ls`, so I looked around. Somewhere on the filesystem, I found a Hexen (IIRC) demo, and decided to download it via Kermit (the only tool/protocol I knew how to use). It took almost a day to finish, but in the end it ran - I was overjoyed. I somehow even found a cheat code for all weapons, and spent a few weeks playing the first 2 levels, while occasionally poking around in the remote system. Then the phone bill came - for 7x more than normal, on top of the ISP subscription - and I lost access to both the Internet and the computer for more than a month. Needless to say, I learned to watch that connection timer like a hawk, and it served me well for the next 10 years before broadband connection was available.
reply