Comments URL: https://news.ycombinator.com/item?id=44314997

Points: 22

# Comments: 2

There is no real need to add an interpreter. Having custom backend s means that while currently it is being used for debug, far in future it might be able to compete with llvm for speed.

Adding an interpreter would be useless as u would still need to write a custom backend.

The problem is llvms slowness for debug and release.

Comptime cannot affect runtime, it cannot do syscalls and cannot go on forever. Due to how limited it is, we can simply let it evaluate and then work with the code that is left.

It is still a better method than either writing text macros[which are also fine but are a pain to use] or using proc macros which can do syscalls and open up a whole new can of worms.

In languages that dont have any metaprogramming support, you must rely on some thing of a generator which is most probably not provided by the compiler vendor and verifying and trusting it is now the responsibility of the user.

Now you are left with things like template metaprogramming where higher and more complex techniques are not supported by the standard or any verification tools and you must trust the compiler to take the right decision regarding the code and having no tools support its verification.

Out of all the options for metaprogramming for a language that must also be verification friendly, comptime is probably one of the best solutions, if not the best.

Zig not being much different from C in this aspect is quite an unexpected compliment because of plethora of work done for its verification. Those same tools can be modified to be used for zig but you would not have to worry about much beyond logic and memory allocation verification [there exists a prototype for both].

Due to how easy to parse and work with the language is, we might see a boom of static analyzers for zig. There are some quite interesting demos that can even go beyond basic borrow checking and straight into refinement types.

Zig's integrated build system will make it easy to add these tools into any project. Or maybe the zig compiler itself will integrate it.

the future is quite hopeful for zig but it is probably not one that is restricted to just borrow checking. I personally think it can go beyond and slowly become what C+FramaC or Ada is now for the critical systems world.

Zig is still not 1.0, theres not much stability guarantees, making something like Frama-C, even tho it is possible is simply going to be soo much pain due to constant breakages as compared to something like C.

But it is not impossible and there have been demos of refinement type checkers https://github.com/ityonemo/clr

Beyond that, tools like antithesis https://antithesis.com/ exist that can be used for checking bugs. [ I dont have any experience with it. ]

source: I was there when it happened and it was GLORIOUS.

oh its about memory safety.

If Ada was used in domains where rust is used, like desktop applications, servers, high perf stuff, it would also do unsafe stuff you could never verify using spark.

But instead it is used in microcontrollers with runtimes provided by adacore and other vendors. Can you fully know if those pieces of code are 100% verified and safe? the free ones are not. atleast the free x86 one.

How ridiculous. The language you use is not memory safe btw. unchecked_deallocation can be easily used without any pragmas iirc. You need to enable spark_mode which will restrict you to an even smaller subset! You cannot even safely write a doubly linked list in it![you can with great pain in rust] [with less pain in Frama-C] [never tried ats]

It could not verify dynamic allocations thats why it has such a huge toolset for working with static allocations.

Frama-C allows you to program in a safe subset of the unsafe language called C.

And these languages are the backbone of everything where lives are at risk. YOu can have a language that allows both unsafe and safe.

Safety is not binary and our trains run C/C++ [BOTH UNSAFE LANGUAGES]

Ada is fine, just verbose, kinda fun, no comments about it except that its kinda sad how weak their formal verification is. I prefer Frama-C over it. You can compare Ada and rust but ada is horrible, sincerely horrible at working with ownership. Frama-C can run laps around it as you can verify EVEN arbitrary pointer arithmetic.

Calling rust a horrible abomination is weird. As someone who dabbled in CL for an year, I love the fact that it has proc macros and even tho its harder to use it, i can make my own DSLs and make buildtime compilers!!

That opens up a world of possibilities.We can actually have safer and stricter math libraries! Maybe put us back in era of non-electron applications?

The horrible part might be syntax but eh, its a stupid thing to care about.