Comment by Eridrus

5 days ago

Why not use Verus?

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

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?

Does it have C parity performance?

  • Verus, not Venus: https://verus-lang.github.io/verus/guide/

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

      8 replies →