On 5/25/23 08:58, Guy Sotomayor via cctalk wrote:
ADA and SPARK (a stripped down version of ADA) are used heavily in
embedded that has to be "safety certified". SPARK also allows the code
to be "proven" (as in you can write formal proofs to ensure that the
code does what you say it does). Ask me how I know. ;-)
I was aware of Ada's requirements in the defense- and aerospace-related
industry. Is that where your experience lies? Is SPARK the "magic
bullet" that's been searched for decades to write provably correct code?
Now, let's hear from the Nim, Zig...etc. enthusiasts. There's a YT
video that claims that Zig code execution is faster than assembly.
Exactly how does that work?
--Chuck