Rendered at 10:09:32 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
skybrian 2 days ago [-]
This looks pretty impressive but it’s all AI-generated (or written in a similar style) and therefore the documentation is lacking.
There is a language specification [1][2] but it lacks coherence.
I think the way to improve it would be to try to teach this language to people and get feedback from them. That is, it needs beta testers. It looks like there’s no community of users yet?
For complete transparency: AI augmented engineering is the core workflow for this project.
I have been pretty diligent about trying to de-slop the project after long RALPH loops and `/goal` prompts, and I review and edit documentation. Based on your feedback, I just made another pass.
Please feel free to let me know if there is anything specific lacking from the docs, and I will update them in the future.
skybrian 2 days ago [-]
If you compare say, the Go language specification for an assignment statement [1] to Salt's explanation of its let statement, there is a big difference. Salt's docs lean heavily on "it works like you would expect from other languages" so you have to reason by analogy. A specification shouldn't work that way; it should actually explain the rules for each language construct, without assuming knowledge of other languages.
Thanks, I restructured that doc and will work on it moving forward.
csb6 2 days ago [-]
For people looking for other languages with statically checked contracts, you might want to check out SPARK, which has been around in some form since the late 1980s. It is a subset of the Ada language and had been used for safety critical code in aerospace and defense projects, as well as for some Nvidia firmware.
It also uses Z3 to discharge proof obligations generated by the contract annotations, and it lets you use swap out different theorem provers as backends.
The GNAT Ada compiler (which is part of GCC) allows you to turn off the dynamic safety checks that are usually inserted into Ada programs at build time so you can optionally remove them if they are proven unnecessary.
SPARK seems interesting. Any ideas how it compares to Salt?
- C performance?
- Generics?
- Syntax ergonomics?
Thanks for sharing!
csb6 2 days ago [-]
Yes, it has generics. The syntax is Pascal-like, which some people used to C-family languages dislike but I personally find nice. Performance can definitely match performant C code. (intended use cases include real-time systems and embedded devices)
It is a way to formally verify Ada, it meets all those criterias.
luckystarr 2 days ago [-]
> [int overflows, etc.] No runtime cost when Z3 can prove it. Otherwise, the compiler emits a safe runtime check as fallback.
Super interesting approach. I see this eventually be integrated into future mainstream languages, though that may take a while. I suspect that the game programming crowd will try to use it first, due to the possibility to prove certain edge cases at compile time and skip the runtime cost. But perhaps this optimization drive is no longer the case because we've got bazillions of cores nowadays. I may be too old for these predictions. Cool nonetheless.
tancop 1 days ago [-]
> I suspect that the game programming crowd will try to use it first
> perhaps this optimization drive is no longer the case because we've got bazillions of cores nowadays
gaming is one of the industries where developers have to care about performance. you can see it with all the backlash on unreal engine, players just dont want slow games even if you ignore the fps chasing pcmr crowd. and getting to 60 or even 30 fps with complex game logic and high res graphics is not easy.
one of the ways you can see this is actually language choice. almost all engines are written in c++ (or sometimes rust). vm languages like java are rare because you dont want gc and extra allocations on the hot path. even for scripting theres a lot of focus on fast and low overhead interpreters, thats why lua is way more popular for games than python or js.
There's a comment saying every function in that file has requires clauses, but... They don't?
Also, the actual implementation of matrix multiply is manually tiled, while the website boasts about automatic loop tiling. It's hard to know what to trust here.
bneb-dev 16 hours ago [-]
Looking. I did a huge purge/rewrite of the benchmarks and this might have regressed. Happy to track here or GitHub.
derdi 12 hours ago [-]
For here (and the website), I would be more interested in trustworthy information about what is actually verified at compile time, and what happens when verification fails.
What if you write a function that takes an array (as an array type if you have one, or as a pointer, or a slice, or whatever). It returns `array[0] + array[1]`, but it has no bounds checks in the code, neither as actual `if` statements nor as `requires` clauses.
Verification of such a function must fail at compile time, right? Does it? What does the error message look like? Someone else found some quote somewhere that seems to suggest that integer overflow checks are implemented as runtime checks if you can't eliminate them at compile time. Does that also happen for bounds checks? If yes, does the user get a warning saying that M out of N checks were moved to run time?
It's just really unclear if you are really doing "Verified safety without the runtime cost." or if you have reinvented Java, which will be just as good (actually better) at eliminating these bounds checks as compile time.
bneb-dev 7 minutes ago [-]
[flagged]
valentynkit 22 hours ago [-]
Bounds and div-by-zero are the easy wins; the real tax with contract systems is the loop invariant Z3 can't infer on its own, where you end up hand-writing an `ensures` longer than the function body. What's the gnarliest invariant you had to spell out by hand to get one of those kernels to verify?
bneb-dev 17 hours ago [-]
For loops already worked but might not have been documented correctly. I just shipped the functionality for `while` loops now, auto-infer works for common cases of invariants:
let mut i = 0;
while i < 5 {
arr[i] = val;
i += 1;
}
So in that case, the compiler detects `i < N` with monotonic increment and synthesizes `i >= 0 && i < N` automatically.
(Works with `<`, `<=`, `i += 1`, and `i = i + 1` via the same mechanism as for-loop induction variables.)
Complex loops (`while i + j < n`, `while p.addr() != 0`) require syntax that I have slopped together an explicit `invariant` keyword that I am not 100% happy with, but will refine later. Z3 checks base case + inductive step via Hoare logic and reports counterexamples on failure.
---
RE: "gnarliest invariant"
`ensures(result != 0)` on the SYN cookie in the kernel contract for the OS project in the monorepo.
derdi 16 hours ago [-]
The more interesting loop invariants aren't the ones about the loop counter but about the contents of the array. If you require `forall i, array[i] == value` after that loop, will the system come up with the loop invariant about the prefix of the array for any given `i`? What about something like bubblesort or insertion sort?
difc 1 days ago [-]
Moving theorem proving upstream into compilers, sandboxes, and the browser seems like the future when we're dealing with increasingly sophisticated AIs. I'm working on similar formal methods but applied to agent sandboxing; do you see Z3 as a better fit than lean? https://github.com/coproduct-opensource/nucleus
Taikonerd 21 hours ago [-]
> Moving theorem proving upstream into compilers, sandboxes, and the browser seems like the future
The way I saw this proposed, back in the 2000s: "proof-carrying code."[0]
The idea is: the compiler compiles the program, and simultaneously generates a proof that the program doesn't violate X, Y, or Z safety rules.
Later, the end-user downloads the program and the proof together, and the local execution environment (the browser, the OS itself, etc) verifies that proof.
The idea being: constructing proofs is hard and sometimes involves manual steps. But verifying a proof is easy and automatic. So do the slow, manual thing once, and the fast thing each time the program is downloaded.
Sounds a bit like Microsoft's Singularity project, though I don't know if they even used a proof system to ensure a program couldn't do bad stuff(TM). After verification they just let the program run in Ring 0 (kernel space) of the CPU to skip even the performance hit of the cpu's isolation.
pocksuppet 19 hours ago [-]
I thought Singularity was just building an OS on a memory-safe language and runtime, C# and .NET.
The same thing Java tried to do with applets at the browser level.
luckystarr 17 hours ago [-]
I listened to an interview with one of the researchers. They had a component to verify "this binary will never allocate mem outside it's allowed area" and by statically verifying that they could enable high performance IPC. Also, that was the source for the decision to allow it to run on Ring 0. That's what stuck in my mind.
psd1 37 minutes ago [-]
Information is sparse about Singularity, which i understand is the same as Midori. Can you find that interview again?
I know about OpenGenera; what left-field OSes might i have missed?
bneb-dev 23 hours ago [-]
Salt chose Z3 because it felt right for a compiler. The 100ms timeout means it's not sound, but it's useful. Lean could be the right choice when a proof is a hard requirement?
rurban 1 days ago [-]
Why no GC? Guaranteed memory safety would be nice
bneb-dev 23 hours ago [-]
It was a design decision. I chose Arenas instead.
The designed arena allocation is both faster and more predictable than GC. The trade-off is that you have to think about memory regions, but you never pay a GC pause.
Eridrus 1 days ago [-]
Why not use Verus?
It augments Rust with Z3 and is not a pile of unverified slop.
bneb-dev 1 days ago [-]
Haven't heard of Venus (the programming language), but it sounds interesting. I'm curious to know what you mean by verified?
Do you happen to know if Venus has a Result type with canonical error codes, pipes, and other ergonomics?
Ah, the issue is that I don't like that syntax: Salt is macro free, and doesn't need assert statements, etc... These are stylistic but I am assuming that under the hood things look quite similar.
I put an effort in to de-slop the project wherever I can. If you've noticed anything specific, I'd kindly request that you open an issue on Github or respond here with your findings so that I might correct them in the future.
Thanks for taking an in-depth look at Salt.
doc_ick 22 hours ago [-]
Thanks for trying to de-slop an ai-created project.
bneb-dev 18 hours ago [-]
Not sure what tone you're going for, but can you expound on what you mean by 'ai-created'?
Hugsbox 17 hours ago [-]
I'm not that commenter, but I feel like you wouldn't have to de-slop the project if it wasn't slop to begin with.
bneb-dev 16 hours ago [-]
My workflow is to design, then use goal and loop prompts to RALPH a feature. At that point, usually there is a bunch of AI generated code that is generally correct but needs refinement, editing, testing, benchmarking, etc... That human-in-the-loop iterative step is the 'de-slop'. Would you prefer different phrasing, or is the trigger here the use of coding agents?
bneb-dev 2 days ago [-]
Salt is a systems programming language that embeds the Z3 SMT solver in the compiler.
You add `requires` and `ensures` clauses to functions, and the compiler proves them at compile time. When Z3 succeeds, the check is elided (zero instructions emitted).
When it fails, you get a counterexample. When it times out (100ms limit per obligation), the check is skipped and counted.
It compiles through MLIR to LLVM and targets KeuOS, a microkernel with an ECS (Entity Component System) architecture. Both are MIT-licensed.
The key difference from Rust/Zig/C: the compiler calls Z3 during normal compilation. No separate verification tool, no annotation language, no proof assistant. The contract syntax is part of the language.
---
What's real
- Compiler: 1,752 unit tests passing, clippy clean. Compiles through MLIR to LLVM IR. x86-64 and ARM64 backends.
- Kernel: 14/14 QEMU e2e tests pass. TCP stack (connect/send/recv/close), ICMP, deterministic builds. NetD (network daemon) runs as a Ring 3 process on SPSC shared memory rings.
- ECS architecture: 13 entity syscalls (402-413). Entity lifecycle (spawn/exit/wait), memory regions as entities (map/brk/alloc), I/O routing via capabilities, socket entity tracking, performance counters, world persistence diagnostics.
- Shell: Inline `ecs`, `ps_ecs`, `free_ecs` commands query ECS World without spawning child processes.
- Benchmarks: Salt vs C (`clang -O3`) on 21 algorithm benchmarks. Salt at parity or faster on 19/21. Allocation-heavy workloads (hashmap, LRU, buffered writer) see 2-10x wins from arena allocation. Compute-bound (matmul, sieve, fib) at 0.9-1.0x of C.
- LSP: VS Code extension ships with semantic tokens, go-to-def, find-refs, Z3 hover.
---
What's not done (research-quality, not production)
- The standard library is incomplete. Many things you'd expect are missing.
- Z3 handles integer arithmetic, bit-vectors, and reals. String and quantifier support is partial. Contracts outside Z3's reach are compile-time checked where possible, silently skipped otherwise.
- Error messages from the Z3 pass can be opaque.
- The kernel targets QEMU (x86-64). Tested on AWS bare metal instances, not local 'bare metal' yet.
- One nights-and-weekends developer.
---
Why this exists
The goal was to find out whether formal verification could be a compiler feature rather than a separate toolchain. The benchmarks say the compiler is fast enough (Lettuce compiles in under a second with contracts enabled). The kernel contracts catch real bugs. But the language hasn't been used by anyone outside the project, and that's the test that matters.
Next time curate what Claude/Codex tells you, this text seems targeted towards you, not a potential user
bneb-dev 19 hours ago [-]
What gives you that impression?
doc_ick 22 hours ago [-]
100%
left-struck 24 hours ago [-]
>One nights-and-weekends developer.
What?
bneb-dev 23 hours ago [-]
This is being made by one person as a side project (not done during core working hours)
Hugsbox 17 hours ago [-]
Why is that a bullet point under "What's not done"? It's confusing in that context, almost as if an AI wrote it and then it wasn't looked over.
bneb-dev 17 hours ago [-]
You could nitpick the subsection title, and from that perspective "What's not done" is a bit of a catch-all for caveats.
With that said, I think it's pretty easy to infer the meaning there.
I'm not really sure how else to be more transparent about things, but I am using an AI-augmented engineering as the core workflow for the project, and that includes drafting docs and this post.
I read and edit the work. For a side-project with no current community support or users, I need to make a judicious decision when to spend time and effort. IMO it is reasonable _not_ to try to trick anyone into thinking that AI is not used. My proof reading and editing will miss things from time-to-time. I'm OK with it at the current scale of the project.
There is a language specification [1][2] but it lacks coherence.
I think the way to improve it would be to try to teach this language to people and get feedback from them. That is, it needs beta testers. It looks like there’s no community of users yet?
[1] https://github.com/bneb/lattice/blob/main/docs/SPEC.md
[2] https://github.com/bneb/lattice/blob/main/SYNTAX.md
I have been pretty diligent about trying to de-slop the project after long RALPH loops and `/goal` prompts, and I review and edit documentation. Based on your feedback, I just made another pass.
Please feel free to let me know if there is anything specific lacking from the docs, and I will update them in the future.
[1] https://go.dev/ref/spec#Assignment_statements
It also uses Z3 to discharge proof obligations generated by the contract annotations, and it lets you use swap out different theorem provers as backends.
The GNAT Ada compiler (which is part of GCC) allows you to turn off the dynamic safety checks that are usually inserted into Ada programs at build time so you can optionally remove them if they are proven unnecessary.
Here are some resources for comparison:
- https://www.adacore.com/languages/spark
- https://learn.adacore.com/courses/intro-to-spark/chapters/01...
- C performance? - Generics? - Syntax ergonomics?
Thanks for sharing!
The language overview can be found here: https://docs.adacore.com/spark2014-docs/html/ug/en/spark_201...
Super interesting approach. I see this eventually be integrated into future mainstream languages, though that may take a while. I suspect that the game programming crowd will try to use it first, due to the possibility to prove certain edge cases at compile time and skip the runtime cost. But perhaps this optimization drive is no longer the case because we've got bazillions of cores nowadays. I may be too old for these predictions. Cool nonetheless.
> perhaps this optimization drive is no longer the case because we've got bazillions of cores nowadays
gaming is one of the industries where developers have to care about performance. you can see it with all the backlash on unreal engine, players just dont want slow games even if you ignore the fps chasing pcmr crowd. and getting to 60 or even 30 fps with complex game logic and high res graphics is not easy.
one of the ways you can see this is actually language choice. almost all engines are written in c++ (or sometimes rust). vm languages like java are rare because you dont want gc and extra allocations on the hot path. even for scripting theres a lot of focus on fast and low overhead interpreters, thats why lua is way more popular for games than python or js.
There's a comment saying every function in that file has requires clauses, but... They don't?
Also, the actual implementation of matrix multiply is manually tiled, while the website boasts about automatic loop tiling. It's hard to know what to trust here.
What if you write a function that takes an array (as an array type if you have one, or as a pointer, or a slice, or whatever). It returns `array[0] + array[1]`, but it has no bounds checks in the code, neither as actual `if` statements nor as `requires` clauses.
Verification of such a function must fail at compile time, right? Does it? What does the error message look like? Someone else found some quote somewhere that seems to suggest that integer overflow checks are implemented as runtime checks if you can't eliminate them at compile time. Does that also happen for bounds checks? If yes, does the user get a warning saying that M out of N checks were moved to run time?
It's just really unclear if you are really doing "Verified safety without the runtime cost." or if you have reinvented Java, which will be just as good (actually better) at eliminating these bounds checks as compile time.
(Works with `<`, `<=`, `i += 1`, and `i = i + 1` via the same mechanism as for-loop induction variables.)
Complex loops (`while i + j < n`, `while p.addr() != 0`) require syntax that I have slopped together an explicit `invariant` keyword that I am not 100% happy with, but will refine later. Z3 checks base case + inductive step via Hoare logic and reports counterexamples on failure.
---
RE: "gnarliest invariant"
`ensures(result != 0)` on the SYN cookie in the kernel contract for the OS project in the monorepo.
The way I saw this proposed, back in the 2000s: "proof-carrying code."[0]
The idea is: the compiler compiles the program, and simultaneously generates a proof that the program doesn't violate X, Y, or Z safety rules.
Later, the end-user downloads the program and the proof together, and the local execution environment (the browser, the OS itself, etc) verifies that proof.
The idea being: constructing proofs is hard and sometimes involves manual steps. But verifying a proof is easy and automatic. So do the slow, manual thing once, and the fast thing each time the program is downloaded.
[0]: https://en.wikipedia.org/wiki/Proof-carrying_code
The same thing Java tried to do with applets at the browser level.
I know about OpenGenera; what left-field OSes might i have missed?
The designed arena allocation is both faster and more predictable than GC. The trade-off is that you have to think about memory regions, but you never pay a GC pause.
It augments Rust with Z3 and is not a pile of unverified slop.
Do you happen to know if Venus has a Result type with canonical error codes, pipes, and other ergonomics?
Does it have C parity performance?
I put an effort in to de-slop the project wherever I can. If you've noticed anything specific, I'd kindly request that you open an issue on Github or respond here with your findings so that I might correct them in the future.
Thanks for taking an in-depth look at Salt.
You add `requires` and `ensures` clauses to functions, and the compiler proves them at compile time. When Z3 succeeds, the check is elided (zero instructions emitted).
When it fails, you get a counterexample. When it times out (100ms limit per obligation), the check is skipped and counted.
It compiles through MLIR to LLVM and targets KeuOS, a microkernel with an ECS (Entity Component System) architecture. Both are MIT-licensed.
---
How it works
Call `safe_div(x, 7)` and Z3 proves `7 != 0`. Check elided.
Call `safe_div(x, 0)` and the compiler stops.
The key difference from Rust/Zig/C: the compiler calls Z3 during normal compilation. No separate verification tool, no annotation language, no proof assistant. The contract syntax is part of the language.
---
What's real
- Compiler: 1,752 unit tests passing, clippy clean. Compiles through MLIR to LLVM IR. x86-64 and ARM64 backends. - Kernel: 14/14 QEMU e2e tests pass. TCP stack (connect/send/recv/close), ICMP, deterministic builds. NetD (network daemon) runs as a Ring 3 process on SPSC shared memory rings.
- ECS architecture: 13 entity syscalls (402-413). Entity lifecycle (spawn/exit/wait), memory regions as entities (map/brk/alloc), I/O routing via capabilities, socket entity tracking, performance counters, world persistence diagnostics.
- Shell: Inline `ecs`, `ps_ecs`, `free_ecs` commands query ECS World without spawning child processes.
- Benchmarks: Salt vs C (`clang -O3`) on 21 algorithm benchmarks. Salt at parity or faster on 19/21. Allocation-heavy workloads (hashmap, LRU, buffered writer) see 2-10x wins from arena allocation. Compute-bound (matmul, sieve, fib) at 0.9-1.0x of C.
- LSP: VS Code extension ships with semantic tokens, go-to-def, find-refs, Z3 hover.
---
What's not done (research-quality, not production)
- The standard library is incomplete. Many things you'd expect are missing.
- Z3 handles integer arithmetic, bit-vectors, and reals. String and quantifier support is partial. Contracts outside Z3's reach are compile-time checked where possible, silently skipped otherwise.
- Error messages from the Z3 pass can be opaque.
- The kernel targets QEMU (x86-64). Tested on AWS bare metal instances, not local 'bare metal' yet.
- One nights-and-weekends developer.
---
Why this exists
The goal was to find out whether formal verification could be a compiler feature rather than a separate toolchain. The benchmarks say the compiler is fast enough (Lettuce compiles in under a second with contracts enabled). The kernel contracts catch real bugs. But the language hasn't been used by anyone outside the project, and that's the test that matters.
---
Links
- Source: https://github.com/bneb/lattice)
- Tutorial: https://github.com/bneb/lattice/blob/main/docs/tutorial/your...
- Architecture: https://github.com/bneb/lattice/blob/main/docs/ARCH.md
- Benchmarks: https://github.com/bneb/lattice/blob/main/benchmarks/BENCHMA...
What?
With that said, I think it's pretty easy to infer the meaning there.
I'm not really sure how else to be more transparent about things, but I am using an AI-augmented engineering as the core workflow for the project, and that includes drafting docs and this post.
I read and edit the work. For a side-project with no current community support or users, I need to make a judicious decision when to spend time and effort. IMO it is reasonable _not_ to try to trick anyone into thinking that AI is not used. My proof reading and editing will miss things from time-to-time. I'm OK with it at the current scale of the project.