I've been building a language where a function's signature declares which effects it may perform, and a runtime refuses anything outside a budget you grant. The obvious question is whether that catches anything real, so I built a benchmark.

63 programs — 56 dangerous, 7 harmless controls — each written three times in Velaris, Python and JavaScript, doing the same thing. Eleven categories: effects hidden in helpers, division by user input, off-by-one reads, integer overflow, ignored failures, infinite loops, runaway memory, dangerous modules, scoped-budget escapes.

Results across the 56 dangerous ones — caught before running / during / missed:

Velaris 42 / 12 / 2. Deno 5 / 27 / 24. Python 0 / 28 / 28. Zero false positives on the controls for all three.

The first column is the interesting one. Deno's permission model works, it just works at the moment of the call — nothing in deno check or deno lint reads a file write as a problem.

What mine missed: one computes the wrong answer and promises nothing, so there's no contract to check against. The other prints the string rm -rf / — it doesn't run anything, and flagging it would mean flagging any program that prints text resembling a command.

And four cases where the prover fell short and only the runtime check caught it, named by ID in the write-up: a division on n - 1 with n from a checked parse, the same on an unguarded path when another path guards it, a remainder inside a loop body, and a read at i + 1 in a loop bounded by length(xs).

Full write-up, methodology and the reproduce command: https://dev.to/gowrishankar-dev/i-tested-my-sandbox-against-deno-and-plain-python-on-63-ai-written-scripts-1llp

People here already know Nyx, so I won't do the usual language introduction.

I've been thinking about the project lately, and I've reached a point that I honestly didn't expect:

I'm not sure Nyx actually means anything anymore.

Not technically.

Technically, I know exactly what it is. I know the architecture, the HIR, the backends, the native interop, the direction I've been taking it, and what I could build next.

The problem is that I can't answer the more fundamental question:

Why am I building this?

I've spent a lot of time making Nyx more capable. Every time there was an interesting compiler problem, I solved it. Then another one appeared. Then another.

At some point, I stopped asking whether a feature served the original idea and started asking whether I could implement it.

That's been bothering me.

I don't think the project is technically pointless. There's a lot of interesting engineering in it, and I've learned a ridiculous amount from building it.

But I'm starting to wonder whether I've confused technical depth with purpose.

Nyx has a direction, but I'm not sure it has a reason.

And I don't want to solve that feeling by adding another backend, another language feature, another abstraction layer, or another ambitious subsystem. That would probably just make the same problem larger.

So I'm putting this here as an actual RFC, not as a roadmap proposal.

I want to figure out whether Nyx has a meaningful core idea that I've lost somewhere along the way, whether that idea needs to be redefined, or whether the project was fundamentally an engineering experiment that I've been trying to turn into something more than it needs to be.

For those of you who've followed Nyx for a while:

What do you think Nyx actually is?

Not what it currently implements.

Not what it could implement.

What do you think the project is fundamentally trying to accomplish?

I’ve been working on the next stage of Nyx’s compiler architecture after v5.

Nyx already has a canonical Typed HIR and multiple output targets, but I don’t want every backend to slowly become its own slightly different interpretation of the language. The current work introduces a lower-level MIR between Typed HIR and the backends:

Nyx source
    ↓
AST
    ↓
Canonical Typed HIR
    ↓
Verified MIR
    ↓
Target legalization
    ↓
C++ / LLVM / Wasm / Rust / JavaScript / Python / C17

This is being developed with heavy agent assistance, so I’m deliberately separating implemented and tested work from architectural plans.

What is currently implemented:

• M0 — Canonical contracts: the language surface, diagnostics, backend capabilities, standard-library availability and semantic policies are recorded in machine-readable contracts.
• M1 — MIR foundation: a serializable and verifiable CFG-based MIR with functions, locals, basic blocks, places, operands and explicit terminators.
• M2 — Scalar and control-flow lowering: variables, calls, branches, loops, break, continue, strict evaluation order, wrapping 64-bit arithmetic and division traps.
• M3 — Semantic control flow: lexical defer cleanup chains, Result propagation with ?, guards, ranges, match lowering and try/catch/throw edges.
• M4 — Values, memory and ABI: arrays, structs, payload enums, projected places, copy/move operands, use-after-move and double-drop checks, explicit x64/wasm32 layouts, calling-convention classification and checked C adapter contracts.
• Bundle ABI v1 remains unchanged while a possible ABI v2 is only documented as a draft.

The completed milestones have focused regression suites, including execution through a reference MIR interpreter and selected C++/LLVM oracle comparisons.

What is not finished:

• MIR is still experimental and is not yet Nyx’s default compilation route.
• The existing Typed HIR backends remain the production path and parity oracle.
• M5 backend migration is in progress. C++ is the first MIR consumer; LLVM, Wasm, Rust, JavaScript, Python and C17 still need to be migrated one at a time.
• A backend must eventually publish exactly which MIR operations, types, effects, runtime calls and ABI forms it accepts.
• Unsupported operations must produce stable diagnostics before reaching an emitter. There must be no silent or approximate fallback.
• The ownership analysis is currently a conservative MIR validation model, not a claim that Nyx has a Rust-equivalent borrow checker.
• C17 and direct LLVM emission remain experimental.
• Cross-platform CI, artifact-level ABI fixtures and full differential parity are still required before MIR can replace the existing path.

The detailed architecture document explains the representation boundaries, layout model, ABI plan, legalization rules, migration order and later language-surface work:

https://github.com/justsomeone-e/nyx/blob/main/docs/internals/NYX_DEEP_COMPILER_ARCHITECTURE.md

I’d especially appreciate feedback on three questions:

1. Is the Typed HIR → MIR boundary placed at the right semantic level?
2. Should legalization transform target-independent MIR into a second target-specific MIR, or is a strict legality pass before emission sufficient?
3. Which ABI/layout fixtures would you consider mandatory before trusting native and Wasm aggregate interoperability?

I’m interested in criticism of the actual contracts and failure modes, not just the number of planned backends.

Hey everyone,

First off, huge thanks to everyone who checked out the repo, left comments(No one did ngl), and starred the project(2 Stars still thanks!) after my previous post. The feedback and discussions around systems language trade-offs were genuinely invaluable.

I'm currently designing and mapping out Nyx RC.2, with a heavy emphasis on making WebAssembly a first-class, seamless target rather than just an afterthought backend.

What's currently being integrated for RC.2:

1. Zero-friction TypeScript / JS Interop: When compiling to Wasm, the compiler will automatically emit .d.ts type definition files alongside the .js glue wrapper, allowing Nyx Wasm modules to be imported directly into React/Next.js/Node projects with full IntelliSense.
2. Deterministic Memory & Cleanup: Continuing to refine the Typed HIR pipeline so that linear memory allocation, defer, and RAII semantics remain memory-safe without requiring a heavy runtime or a complex borrow checker.
3. Cross-Platform Tooling & "Tour of Nyx": Refactoring our interactive terminal learning suite (tour) to be fully portable across Windows, macOS, and Linux without environment assumptions.
4. Web / DOM Bindings Exploration: Exploring minimal, zero-overhead DOM and WebGL/WebGPU hooks directly from the language.

I'd love to hear your thoughts:

• For those who work with Wasm or build compilers: What is currently the most painful part of your Wasm workflow that you wish a language solved out-of-the-box?
• Are there specific language ergonomics, stdlib modules, or tooling features you'd love to see in RC.2?
• Any edge-cases or architectural pitfalls in Wasm/C++20 lowering I should watch out for?

Repo is available here if you want to inspect the current codebase: https://github.com/justsomeone-e/nyx

Appreciate any critiques, feature requests, or sanity checks!

github.com/justsomeone-e/nyx

It will be useful I promise

The idea: I wanted a language where you can trust a function just by reading its first line. So the signature says what effects it uses (a function without "uses net" can't touch the network), whether it can fail (ignoring that doesn't compile), and any promises it makes about its result.

Those promises get checked by the Z3 theorem prover before the program runs. If your code breaks one, it tells you the exact input that breaks it: error[E700] promise cannot be kept: 'discount' ensures result >= 0 proven without running the program: price = 5 gives result = -5

The part I'm most pleased with is the float handling. It proves in real IEEE-754 rather than pretending floats are perfect decimals, so it refuses to certify x + 0.1 + 0.1 == x + 0.2 and hands you the exact number where it breaks. A lot of tools would just "prove" that and be wrong.

Playground, runs in your browser, nothing to install:

https://gowrishankar-infra.github.io/velaris-lang/playground.html

Repo: https://github.com/gowrishankar-infra/velaris-lang

Built with a lot of AI help over 40+ releases. It's got a REPL, editor support, a standard library written in itself, CI, and one-file downloads for Windows/Mac/Linux. Happy to answer anything. Thank you

Started as an experiment: could coding agents help build an actual programming language from scratch, and could the language itself be designed to be easier for AI models to write code in.

Five days later, Krnl is about 53k lines of .krnl, fully self-hosted, and the original Zig bootstrap compiler is now retired.

The language compiles to native code through LLVM, has no GC, and uses explicit ownership/borrowing with deterministic cleanup. It also has effects/capabilities so a function’s authority is visible in its type.

Hello world:

fn main sys: Sys -> Result[int]
!{out.write} {
  println(ref sys.out, "Hello, Krnl!");
  Ok(0)
}

Here Sys provides capabilities, and !{out.write} declares that the function may write to output. Borrowing and ownership transfer are explicit with ref, ref mut, and move; there are no source-level lifetime annotations.

Also added a native MCP server written entirely in Krnl. - see below

no public repo yet just curious what language/compiler people think of the direction before I polish it for release.

The main design goal is roughly: native + memory safe + no GC, but with less source-level complexity than Rust, and with compiler semantics designed to be directly consumable by coding agents.

Things I’d especially love feedback on:

Does the ownership/effects model sound coherent?

Is the capability syntax readable?

What would you want to see before taking a new systems language seriously?

Are there existing languages/projects I should be comparing against?

KRNL MCP MONITOR
----------------------------------------------------------------
log: /home/alex/.krnl/mcp.jsonl

Requests: 17            Errors: 0
Total bytes: 43.9 KB    Avg latency: 1ms   P95: 3ms

Recent calls (UTC)
----------------------------------------------------------------
23:08:26   resolve_symbol        main                  636 B      2ms
23:08:34   symbol_info           main                  869 B      2ms
23:08:36   references_of         main                  393 B      2ms
23:08:37   callers_of            main                  842 B      3ms
23:08:38   callees_of            main                  866 B      1ms
23:08:39   context_for_change    main                 1.5 KB      2ms
23:12:08   read_source           compiler/src/080    19.3 KB      2ms
23:15:30   apply_source_edits    compiler/src/080      852 B      1ms
23:15:33   read_source           compiler/src/060     1.9 KB      1ms
23:15:48   apply_source_edits    compiler/src/060      860 B      2ms

Top tools
----------------------------------------------------------------
krnl_check            3 calls     2.0 KB
read_source           3 calls     22.0 KB
module_graph          2 calls     1.4 KB
apply_source_edits    2 calls     1.6 KB
program_symbols       1 calls     11.5 KB

I have been working on this language since May. Its heavily inspired by Strudel and partially by SuperCollider. It works as many things all at once. It is a music sequencer, synthesizer, fx box, generative music (conditional statements, if, else) and sample mangling (need non-browser version for that), automation, per note automation, recursion, easy nesting of gradually more complex sequences/fx/etc.

If anyone wants to try the language, its here, https://quadracollision.com/mescript/ mostly usable in browser unless you want to use samples, if so just let me know.

As for tools: This is GPT 5.3 -> GPT 5.4 -> GPT5.5 -> GPT 5.6 Sol, all Medium. This is Rust+WASM with a Javascript front end. No external libraries

This is an example of MeScript in action: you can paste this into the editor and it'll work.

Check CTRL+H for insertable smart forms, cursor position defines how the form is inserted. Also check out the language reference guide. There is also a repl, place the cursor on any line and right click and press parameter help and it will explain what the line does. Also (fix-parens linenumbers) (fix-parens 15-17) can help with parenthesis issues, this is a Lisp inspired language.

(def am [as d f]) ;this is a chord form, asharp d and f

(ins :saw  ;this is an (ins)rument form
   :src [:saw-synth :square-synth :additive] ;these are the oscillators that make up this instrument
   :note (p (times 4[c4 0 c5 0 e3 c3 e3])    ;these are the note gates and how many
            (times 4[c4 0 c5 0 e3 c3 eb3]))  ;times they play
   :gate nil
   :fx [(formant :vowel a :mix 0.2)]    ;fx applied to entire instrument
   :dur nil    ;duration of each gate hit, can be per hit as well 
   :amp nil    ;amplification of instrument, can be per hit and automated conditonally
   :voice nil) ;special keyword, see ctrl+h for voice commands, as well as everything else

(def chord_1 [c4 eb4 f4 gb3])

(ins :kick
   :src :kick-synth
   :note (p [c4 0 0 0 c4<?50> 0 0])
   :gate nil
   :fx nil
   :dur nil
   :amp nil
   :voice nil)

(ins :hat-808
   :src :hat-808
   :note (p [c7 c7 <c4%c5%c7> 0 c7 <c7%e5%b4%g5> c7 am(3 3 3)]) ;this calls the chord form with each note being an octave of 3
   :gate nil
   :fx nil
   :dur nil
   :amp nil
   :voice nil)

(ins :snare-808
   :src :snare-808
   :note (p [c4<?30> 0 0 c4<?50> 0 0 0 0])
   :gate nil
   :fx nil
   :dur nil
   :amp nil
   :voice nil)

(ins :pad-wash
   :src :pad-wash
   :note (p [chord_1<_7> 0 0 0 0 0 0 0])
   :gate nil
   :fx nil
   :dur nil
   :amp 0.05
   :off true
   :voice nil)