3 ms·
GNAT is a frontend (written in Ada yes) to GCC which might be one of the strangest pieces of C++ code in this world. And don't go there with AdaCore's SPARK exa
by touisteur 5y ago
GNAT is a frontend (written in Ada yes) to GCC which might be one of the strangest pieces of C++ code in this world. And don't go there with AdaCore's SPARK examiner/prover implementation either because it's mostly an Ada frontend to Why3 (I'm simplifying) and you don't want to know what's behind Z3, CVC4 and Altergo. I'm a huge fan of SMT tech but I'm glad I don't have to open the hood.
These tools are enablers. Would it be nice to have an all-Ada compiler? Well, no! I want most of the gcc engineers to work for me! As long as the gcc backend improves, I get more perf! As long as SMT tools improve I get faster automated proof of contracts, or automated proof of far more complex contracts!