Vx 0.0.1: placement in the type system

10 September 2026

A machine is no longer one processor. It is a CPU, a GPU, sometimes a neural accelerator, and half a dozen memory spaces with different capacities, different bandwidths, and different rules about who is allowed to read them. Most languages treat all of that as infrastructure. Vx treats it as types.

The machine has a shape

A single node, drawn as the hardware actually arranges it:

      CPU                            GPU
 +---------------+           +-----------------------+
 |               |   PCIe    |                       |
 |   CPU_DRAM    | <=======> |        GPU_HBM        |
 |    128 GiB    |  63 GB/s  |  80 GiB @ 3.35 TB/s   |
 |               |           |                       |
 +---------------+           |  +-----------------+  |
                             |  |      SMEM       |  |
                             |  |   228 KiB / SM  |  |
                             |  |    128 B/cyc    |  |
                             |  +-----------------+  |
                             +-----------------------+

Three memory spaces, three capacities, three very different bandwidths, and one edge between them that costs something to cross. SMEM is not a separate pool sitting beside HBM — it is a small, fast region inside it, private to one streaming multiprocessor, and there are a hundred and thirty-two of them. The ratios are what matter: SMEM is roughly four thousand times smaller than HBM, and the link to the host is fifty times slower than HBM itself.

Every one of those numbers is in a vendor datasheet. None of them are in a type.

In C++ all three spaces produce the same thing: float *. SYCL and Kokkos type which region within a device — registers, scratchpad, DRAM — but neither types which device, so two allocations on two GPUs are indistinguishable to the type system.

That is a ceiling rather than an oversight: a library can only type what a template parameter carries, and where code runs is not part of a C++ function's type.

So the structure above exists in the hardware, in the documentation, and in the programmer's head. The one place it does not exist is the program.

Putting it in the type

A tensor's type carries its element type, its shape, and the memory space it lives in. A spawn on block names the device it runs on. Here is a matmul on an accelerator, written out in full:

// Two matrices already resident in NPU memory.
fn custom_matmul(
    a: Pinned<Tensor<f32, [4, 4]>, Topology::NPU[0]>,
    b: Pinned<Tensor<f32, [4, 4]>, Topology::NPU[0]>)
    -> Verified<Tensor<f32, [4, 4], Memory::NPU_HBM>> {

    let mut result =
        Tensor<f32, [4, 4], Memory::NPU_HBM>::uninit();

    // Dispatch the computation to the accelerator.
    spawn on(Topology::NPU[0]) {
        for i in 0..4 {
            for j in 0..4 {
                result[i][j] = 0.0;
                for k in 0..4 {
                    result[i][j] += a[i][k] * b[k][j];
                }
            }
        }
    }

    return Verified(result);
}

Read the signature and the whole placement story is there. Pinned<T, Topology::NPU[0]> says both operands already live where the accelerator can reach them, so the function cannot be called with a host tensor by accident. The return type says the result is in NPU_HBM, so a caller that wants it on the host has to say so. And Verified<T> carries the fact that the value has been checked, in the type, rather than in a comment.

None of that is a runtime check. It is the signature.

What happens when the placement is wrong

Take the same idea and forget one transfer. The compiler names the space the value is in, the spaces the device can see, and the fix:

Error[E6003] at 13:9: 'a' 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 last clause — cost 50 on the declared path — is there because the compiler also knows what the move costs, over the machine you described to it. The same declaration that makes the error possible is what prices the fix.

What it checks today

These are implemented, have diagnostic codes, and are held by tests:

Check	Rules out
Address-space visibility (`E6003`)	A device reading a space it cannot address; a host reading device memory
Capacity admission (`E6009`, `E6010`)	A tensor larger than its space; a working set that fits tile by tile and not together
Transfer reachability (`E6002`)	A move between spaces with no declared path
Borrow checking	Aliasing and lifetime errors, with region tracking
Linear types	Use after move of a consumed buffer
Seam contracts	Reading a buffer whose asynchronous transfer is not yet visible; discharged by z3

The machine itself is a source file. fleet/ holds twelve of them — A100 in both memory sizes, H100, H200, B200, MI300X, an Apple M4, multi-GPU nodes — each eight to twenty-four declaration lines, each citing its sources and marking unverified figures as unverified.

It is a cross compiler

The machine Vx targets is declared, not detected. --host names the CPU and --machine fleet/<sku>.vx names the accelerator, so the compiler is not limited to the box it is running on. A100 binaries get built on an x86 EC2 instance and shipped to the GPU machine.

This matters more than it sounds. A previous --target flag was removed precisely because it stamped one triple across a whole module, including main — which produced modules that were wrong about the machine they named. Declaring the host and the device separately is what replaced it.

What is not built

This is 0.0.1, and the number is meant literally.

The standard library is thin. There is a Vec, a HashMap, iterators, some maths. There is no package manager and no ecosystem.
There is no while loop. for over a range, and recursion, are what exist.
grad() is young. Automatic differentiation runs through Enzyme and works, but it currently accepts differentiation of a discrete-valued function, which is not a meaningful thing to ask for.
The calculus behind the placement checks is a design with tests, not a soundness theorem.
Some documents in docs/ describe designs rather than code, and say so where that is true.

0.1 is being saved for the release that has a standard library worth the name. Until then the version stays in 0.0.x, where it can move as often as it needs to.

Trying it

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

macOS on Apple Silicon and Linux x86_64. LLVM 22 has to be present — Vx lowers through MLIR and drives mlir-translate, opt, llc and clang from it, and a different major version will not do, because the MLIR C API changes between releases. The installer checks before it downloads anything and tells you the exact command if something is missing.

The language tour is the fastest way to see whether the idea appeals. The documentation covers the type system, ownership, the heterogeneous model and machine files, and every code example in it is compiled by CI — a previous audit found a tutorial teaching syntax that had never been implemented, so now the build fails rather than the reader.

Vx is Apache 2.0 with the LLVM exception. Bug reports are the most useful thing you can send: github.com/vx-lang/Vx/issues. If you want to work on the compiler, the issues labelled good first issue each state the problem with a reproduction you can run.