Birbla

Join the discussion

Write your take first — we'll ask for email only when you're ready to publish.

Sign in
  • Hacker News
  • Why not use Verus?

    It augments Rust with Z3 and is not a pile of unverified slop.

    by Eridrus
  • Why no GC? Guaranteed memory safety would be nice
    by rurban
  • 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
    by difc
  • 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?
    by valentynkit
  • I was confused by the matrix multiply example since it doesn't show requires clauses. So I looked at what is presumably the source I'm supposed to look at: https://github.com/bneb/lattice/blob/main/basalt/src/kernels...

    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.

    by derdi
  • > [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.

    by luckystarr
  • 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.

    Here are some resources for comparison:

    - https://www.adacore.com/languages/spark

    - https://learn.adacore.com/courses/intro-to-spark/chapters/01...

    by csb6
  • 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?

    [1] https://github.com/bneb/lattice/blob/main/docs/SPEC.md

    [2] https://github.com/bneb/lattice/blob/main/SYNTAX.md

    by skybrian

Explore Birbla archives