[ScottMoore0]

A draft, for consideration: take it, change it or close it. It adds 8- and 16-bit word types to Base. I know bytes are U32 by ruling today (tests/base/bytes_ops.bend, and File.read_bytes/TCP.send_bytes take List<&2, U32>), so this is an option, not a request to change that.

Why it might be worth having. A typed byte makes wrapping at 8 bits, byte order and range part of the type, which suits proofs about encodings: UTF-8, checksums, crypto, wire formats. Several hub packages build their own version today.

What it adds (250 lines of base.bend, plus a test):

• type Byte is Data: Byte{data: Word(8n)} and type Word16 is Data: Word16{data: Word(16n)}, built the way U32 is:
  • add sub mul and or xor not inc shl shr, which wrap;
  • cmp is_eq is_lt is_le is_gt is_ge;
  • to_nat to_u32 from_nat show.
• U32.to_byte and U32.to_word16, which keep the low bits.
• U32.byte(a, i), byte i of a, least significant first.
• U32.of_bytes(b0, b1, b2, b3), least significant first, and U32.of_bytes_be, most significant first.
• Word16.of_bytes.
• Word.lo, Word.hi and Word.cat, to split a Word(m + n) and join it back.
• One law, Byte.to_u32_to_byte: U32.to_byte(Byte.to_u32(b)) == b, proved by cases on the 8 bits.

There are no natives, so these run as Base defs in every lane. Natives can follow if you want them.

The names. U8 and U16 would be the natural names, but 11 hub packages declare their own U8 (3 also declare U16). A redeclared Base name is refused (#1042), so those packages, and 6 files that import them, would stop checking. Eight of the 11 are UTF-8 decoders where U8 is the decoder's state, not a byte. Byte and Word16 collide with nothing:

• I checked every one of the 52 type, constructor and def names against all 647 packages on the hub (pulled today, hash-verified) and against the repo's tests, demos, benches and Base.
• As a stronger check, every hub file that mentions any of the names (107 files) gives the same --check-only output with this Base as with main's.

Tested on main at e5527d5:

• tests/base/byte_word16.bend: the interpreter, JS and C lanes all print the expected line, and --verdict prints ALL PROOFS CHECK. So does Base on its own.
• All 1,665 test files: --check-only output is identical with this Base and with main's.
• Cost: Base grows by 8%, which adds roughly 5–10 ms to every check (about 113 ms against 121 ms, averaged over warm runs on a one-law file; the gap is close to run-to-run noise).

Not run: gates/test.ts and gates/safe.ts on the minis.

If you'd rather not grow Base, I'll publish it as a hub package instead.

Found and tested with Claude Code, running Claude Opus 5.5, during an audit of --verdict.

[Lorenzobattistela]

Thanks, this is clean and well tested, and the naming survey against the hub is exactly the check we'd want.

We're going to keep Byte out of Base for now. Base's byte APIs (File.read_bytes, TCP/UDP, args_bytes) all take and return U32, so a Byte type there would be a second representation that nothing in Base produces or consumes. Every check would pay for it (Base +8%, and 52 names reserved for every module under #1042) while most programs never touch it. Without natives it would also be too slow to be the I/O representation.

We may add something like this in the future, but for now we're focused on keeping Base small and concise.

Please do publish it as a hub package. That gives the packages rolling their own U8 one shared, proved byte type, and if byte I/O ever moves off U32 we'd design Byte in Base together with its natives and start from yours.