There have been informal comparisons by researchers between the use of SPARK and Frama-C, but these are not enough to really understand the most important differences at the heart of the these different toolsets for formal verification of programs. Another interesting point of comparison is the Why3 technology which underlies both SPARK 2014 and Frama-C (when using the Jessie plugin instead of the WP plugin for deductive verification). Hence the interest of this article we have written for the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, which goes into deeper difference in design choices between these technologies, in terms of executability, semantics of logical parts, use of ghost code, and generation of counterexamples.