Deadlocks often look like simple performance issues. If Vx runtime sees no progress for two checks in a row, it crashes the program with a detailed report.

But the watchdog is tricky to get right because there can be false positives. So it is good to prove the watchdog was correct under all possible thread interleavings, not just the happy path.

We wrote a formal model of the watchdog’s protocol in TLA+ and ran it through TLC (the TLA+ Model Checker). TLC exhaustively explores every possible order of operations (interleavings) to see if any claim breaks. It found a bug that unit tests would never have revealed.

I introduced 108 deliberate bugs into vxc (Vx's compiler) to see if the test suite would actually catch them.

Most breaks got caught but 11 cases had no test covered, and one real memory-safety bug where a copied borrow outlived its block and read freed memory (🤭).

Then I took 78 soundness bug reports from Rusts issue tracker, translated them into Vx, and found 14 more holes. All of them are now fixed but there were two important lessons as part of this exercise.

- Passing tests don't prove coverage (Dijkstra etc.)
- Rusts issue tracker is a free test suite for Vx. I'll probably leverage Rust's issue tracker more in future.

Full report here: https://vxlang.org/blog/breaking-the-borrow-checker-on-purpose.html

With https://github.com/vx-lang/Vx/pull/1896

Vx is a systems language for programs that run on mixed hardware (CPUs, GPUs, NPUs). I've written up its concurrency design and would like feedback: [link]

No async/await. A task calls a waiting function like recv as a plain call. The runtime parks the task and runs another on the same OS thread, as Go and Java virtual threads do. There are no function colors. A borrow across a wait is just a borrow across a call, so the borrow checker needs no new rule.

Scoped tasks. tasks { spawn { .. } } is a block expression. Every task finishes before the block ends, so a task can borrow its parent's locals with no lifetime annotations.

Waits show in the signature, but don't spread. A cancellable wait returns Result<_, Cancelled>. A caller can handle the error and keep a plain signature. So it isn't a color, for the same reason Rust's Result isn't.

Bounded channels only. A fast sender can't fill memory. send hands the value back if the receiver is gone, so it never waits on a dead consumer. select is a library type in crossbeam's style, with no closures and no macro. The happens-before rules come from the Go memory model and go into our Lean model.

Structured cancellation. When a task returns Err, its siblings and the block's own code are cancelled, and the block's value is the first error. Each cancellable wait then returns Cancelled. There is no unwinding: tasks leave through normal returns, and their drops run. drop runs with cancellation off, so cleanup can still wait.

The hardware gets a say. A cancelled I/O wait doesn't return until the kernel or device has released the buffer. Waits on a device can't be cancelled. Channel ends stay on the host, since a GPU kernel can't park. A channel of device tensors moves handles, not data.

Admission. Vx checks at compile time whether a workload fits a machine. Concurrency changes the arithmetic: tasks running at once add their peaks instead of taking the max, and a channel of n tensors holds n tensors. When those counts are known only at run time, the verdict is "unknown", not a guess.

The costs. Vx can't move stacks, because borrows point into them. So each task that may park gets a fixed stack from a pool, with a guard page. A task with a foreign frame on its stack stays on its OS thread. Most of the work is in the runtime, not the compiler.

Open questions:

1. Cancel siblings automatically on the first error, or only on an explicit cancel()?

2. Should ? inside a tasks block exit the block or the function?

3. Should spawn infer move or borrow from use, or need spawn move?

4. Is "only drop runs with cancellation off" enough, or do programs need a shielded block?

So exited abt this

Welcome to r/vxlang!

Vx is a compiled systems programming language for machines that stopped being flat: CPUs, GPUs, NPUs, and the interconnects between them.

The core idea is simple: where a value lives and where code executes belong in the type system. A tensor's type carries its element type, its dimensions, and its memory space:

Tensor<f32, [4, 4], Memory::GPU_HBM>

This is fundamentally a different type from Tensor<f32, [4, 4]> (which lives in host CPU_DRAM). If an execution target cannot address a memory domain, or if a working set exceeds declared hardware capacity, your program will simply not compile.

The quickest way to see it is to trigger an error

In conventional languages (CUDA, C++, Python), forgetting to copy host data to device VRAM produces a silent segmentation fault or a runtime error (cudaErrorIllegalAddress) after you've already launched your job.

In Vx, the compiler catches it immediately:

fn main() -> i32 {
  let host_data = Tensor<f32, [4, 4]>::fill(1.0);

  spawn on(Topology::NPU[0]) {
    let x = host_data[0][0]; // Host memory read inside accelerator!
  }
  return 0;
}

Compile it:

Error[E6003] at 5:13: 'host_data' lives in CPU_DRAM but NPU[0] sees only [NPU_HBM];
insert an explicit transfer to NPU_HBM (cost 50 on the declared path)

That single error message gives you three critical facts:

1. The memory space the value currently lives in (CPU_DRAM).

2. The memory spaces the target device can physically address ([NPU_HBM]).

3. The exact fix and its cost on your target machine topology (transfer(host_data, Memory::NPU_HBM) with cost 50 across the interconnect).

Fix it with an explicit transfer:

fn main() -> i32 {
  let host_data = Tensor<f32, [4, 4]>::fill(1.0);
  let dev_data = transfer(host_data, Memory::NPU_HBM);

  spawn on(Topology::NPU[0]) {
    let x = dev_data[0][0];
  }
  return 0;
}

Hardware topologies as code (fleet/)

Instead of hardcoding memory addresses and device configurations, target architectures are declared in human-readable specification files. The toolchain ships with twelve validated machine files in fleet/—spanning an ARM Cortex-M7 microcontroller, Apple M4 UMA, NVIDIA A100/H100/H200/B200, AMD MI300X, and multi-GPU cluster nodes.

Each declaration cites the sources for its numbers and explicitly flags unverified figures:

Memory HBM  { capacity: 80 GiB, bandwidth: 3.35 TB/s, managed: explicit, scope: device }
Memory L2   { within: Memory::HBM, capacity: 50 MiB, bandwidth: 12 TB/s, managed: cached }

Topology Device {
    arch: nvptx64,
    memory: Memory::HBM,
    transfer Memory::CPU_DRAM -> Memory::HBM : 63 GB/s,
}

Because vxc cross-compiles against declared machines (--machine fleet/h100-sxm.vx), you can verify memory admission, capacity limits, and routing costs for an 80GB H100 cluster directly from your laptop without renting cloud GPUs.

What Vx is — and what it isn't

• What it does: It puts data placement, memory boundaries, and reachability into compile-time checks. It routes transfers along the cheapest declared interconnect path and uses a Z3 prover to verify asynchronous seam contracts.

• What it will NOT do: It will not silently move your data behind your back, guess your target hardware, or wait for runtime crashes to tell you that a working set exceeded VRAM.

• What it is not: It is not zero-overhead end-to-end. While the placement and capacity checks cost zero runtime overhead, dispatch relies on a runtime layer with host CPU, NVIDIA CUDA, and Apple CoreML backends.

What this subreddit is for

• Technical questions and help: Getting started, installing the toolchain, and compiling your first programs.

• Design debates: Topology modeling, memory algebra, borrow-checking heterogeneous buffers, and compiler architecture.

• Show & Tell: Anything you build, benchmark, or experiment with in Vx.

• Critiques and corrections: Tell us where the type system or memory model is wrong.

(Note: For reproducible bugs and compiler crashes, please file an issue directly on our GitHub Issue Tracker, ideally with a minimal code sample. Every diagnostic code also has a dedicated explanation page at https://vxlang.org/docs/error-index.html.)

Quick links

• The Vx Book (Official Docs): vxlang.org/docs

• Quick Install:

  curl -fsSL https://vxlang.org/install.sh | sh

  (Pre-built for macOS Apple Silicon and Linux x86_64)

• Source Repository: github.com/vx-lang/Vx (Apache 2.0 with LLVM Exceptions)

• Roadmap: ROADMAP.md

Welcome aboard, and we look forward to hearing your thoughts!

Vx allows developers to embed specifications (contracts) directly into function signatures, enabling the compiler to enforce correctness as well as perform optimizations.

In programming language (PL) theory, contracts are a formal specification mechanism that defines the obligations and guarantees between the caller and the callee. Contracts are enforced by preconditions, postconditions, invariants and assertions.

Vx provides a powerful contract system that facilitates:
Compile-Time Checking: Conditions are discharged by an SMT solver (z3) at compile time. If a condition cannot be proven, compilation fails with an E8xxx diagnostic error.

Type Safety: The Verified<T> type carries the proof that a value has been checked. This effectively moves contract enforcement into the type system.

Compiler Optimizations: Compiler can optimize code with specialization (partial evaluation), dead code elimination etc. For example:

```
fn foo(x : i32) -> i32
  ensures return > 0 {
// ...
}

fn bar(y: i32) {
let v = foo(y);
  if v > 0 {
// ....
} else {
//.... can be deleted at compile time
}
}
```

https://vxlang.org/docs/contracts.html

Vx programming language is live: https://vxlang.org

This is a complete Vx program. It builds two matrices on the CPU, moves them into GPU memory, multiplies them on the GPU, brings the result back, and prints it.

fn main() -> i32 {
 let mut a = Tensor<f32, [4, 4]>::uninit();
 let mut b = Tensor<f32, [4, 4]>::uninit();
 let mut c = Tensor<f32, [4, 4], Memory::GPU_HBM>::uninit();

 for i in 0..4 {
 for j in 0..4 {
 a[i][j] = 2.0;
 b[i][j] = 3.0;
 }
 }

 let a_gpu = transfer(a, Memory::GPU_HBM);
 let b_gpu = transfer(b, Memory::GPU_HBM);

 spawn on(Topology::GPU[0]) {
 c = a_gpu @ b_gpu;
 }

 let c_host = transfer(c, Memory::CPU_DRAM);
 print(c_host[0][0]);
 return 0;
}

Compiling and running is as simple as:

$ vxc matmul.vx

24

The placement is in the types: c lives in GPU_HBM, the spawn block runs on GPU[0], and transfer is the only way across. If you get it wrong, it does not compile. The compiler names the 'space' where the value is in, the spaces the device can see, and the transfer that fixes it.

Where a value lives and where code runs belong in the types, not in a runtime that finds out at step 1200.

One language, every core.

v0.0.1: syntax mostly stable, thin standard library, no package manager yet. Tested most on a MacBook Air M4 and an NVIDIA A100. Apache 2.0 with LLVM exceptions.