bneb-dev

6 ms·

1.
by bneb-dev 2mo ago
Ok take a short break from Claude 5.0 to take a look at the real future of software engineering.
2.
by bneb-dev 3mo ago
Made updates directly influenced by your input. Please feel free to follow up in Github! See https://github.com/bneb/lattice/blob/main/docs/deep-dives/z3...
3.
by bneb-dev 3mo ago
With 92 contributors, I'd bet that The Vera Project is much more mature. Salt has some different ergonomics and performance goals though, which makes this project unique.
4.
by bneb-dev 3mo ago
Agree with your overall point. I made some changes to extend the current paradigm a bit: https://github.com/bneb/lattice/blob/main/docs/tutorial/09-c... --- Invariants aren't always inferr
5.
by bneb-dev 3mo ago
LH seems cool but the syntax would definitely take some getting used to...
6.
by bneb-dev 3mo ago
It looks like verification is distinct from the compiler.
7.
by bneb-dev 3mo ago
I'm not sure what the point of bringing up Versus is. Is it https://verus.io/ ? Is it a plug for your own project? There are several points you made where I think we just fundamentally disagree so I'll decline to
8.
by bneb-dev 3mo ago
Looking. I did a huge purge/rewrite of the benchmarks and this might have regressed. Happy to track here or GitHub.
9.
by bneb-dev 3mo 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-t
10.
by bneb-dev 3mo 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 e
11.
by bneb-dev 3mo 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 +=
12.
by bneb-dev 3mo ago
Not sure what tone you're going for, but can you expound on what you mean by 'ai-created'?
13.
by bneb-dev 3mo ago
What gives you that impression?
14.
by bneb-dev 3mo 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?
15.
by bneb-dev 3mo 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.
16.
by bneb-dev 3mo ago
This is being made by one person as a side project (not done during core working hours)
17.
by bneb-dev 3mo ago
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
18.
by bneb-dev 3mo 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?
19.
by bneb-dev 3mo ago
Thanks, I restructured that doc and will work on it moving forward.
20.
by bneb-dev 3mo ago
SPARK seems interesting. Any ideas how it compares to Salt? - C performance? - Generics? - Syntax ergonomics? Thanks for sharing!
21.
by bneb-dev 3mo ago
Thanks for reading and sharing your thoughts!
22.
by bneb-dev 3mo ago
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.
23.
Show HN: Salt – a systems language with Z3 theorem proving in the compiler(salt-lang.dev)
44 points by bneb-dev 3mo ago|54 comments
24.
by bneb-dev 3mo 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 instructi
25.
Show HN: Trytet – Deterministic WASM substrate for stateful AI agents(trytet.com)
3 points by bneb-dev 6mo ago|0 comments
26.
Show HN: Parsing hostile industrial data in 64MB WASM sandboxes(ingelt.com)
2 points by bneb-dev 6mo ago|0 comments
27.
Show HN: Autonomous Prover Running > 1hr(perqed.com)
4 points by bneb-dev 6mo ago|0 comments
28.
Show HN: Aacyn v0.7.0 – A bare-metal observability engine (5M events/SEC)(aacyn.com)
1 points by bneb-dev 6mo ago|0 comments
29.
Show HN: Write and Run Salt v0.9.2 in the Browser(salt-lang.dev)
3 points by bneb-dev 7mo ago|0 comments