I am pretty sure serious projects like tigerbeetle freeze a version [most probably latest release] and use it. nightly is for experimental stuff.
116 karma · joined December 2, 2021
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.
cmon, lets not lie.
300 is clearly a bigger number than 40, so was the attack wrong? india used it as an excuse to kill more people than what should be considered a good proportional response!
Since that attack[and other operations], JeM and others became fairly inactive and terrorist attacks have gone down by an insane number, what used to be a daily occurrence and a reason to not attend local festival celebrations due to threat of bombs is now a rarity.
Proportionality has nothing to do with defence. Why on earth would u kill only a few terrorists as a response? Israels actions are fucked up but proportionality does not apply to defence. If a state is retaliating to a threat, why would it leave the threat alive, which would only cost lives of more of its people?
Israel's airstrike policy is bad and roof knocking is not enough, the way israel conducts war is wrong and there needs to be intervention that is able to chain israel while eliminating hamas, demilitarising palestinian jihadist groups and stabilising the region.
But proportionality has nothing to do with defence. you can be disproportional if that means the threat ceases to exist.
In all 3, you gotta verify [frama-C, astree,bedrock, the many projects working on rust, esp the coq one] and extensively test it.
But by default, all 3 provide a different level of gurantees
Proportionality has nothing to do with self defense.
Hamas the org was involved, and the other ones too, they are the target.
But I do agree that Israel's policies regarding air strikes are fucked up
create a separate state for palestine under the control of hamas would only legitimise them, allow them to easily get more weapons and go on another oct 7, which will again lead to the bombings currently happening.
Bombing them to death would lead to deaths of many, many women and children cuz gaza is 75% children.
You cannot have peace with hamas, only ceasefire, and even then they havnt stopped launching homemade missiles.
The most sane solution is defeating hamas, establishing a third party control over it to stabilise the region and then return it to democracy, but israel is too trigger happy to do any progress on this field and hamas wants all of israel.
You cannot have peace on the land without destroying hamas. Not even for moral reasons. Maybe there is another solution in ur mind?