SPARK [0], to put it simply. Contracts and static analysis rather than runtime checks takes Ada from being good to being great. I do prefer GNAT's error messag

SPARK [0], to put it simply. Contracts and static analysis rather than runtime checks takes Ada from being good to being great. I do prefer GNAT's error messages over AdaCore's compilers (despite the compiler frontend still being based on GNAT), but SPARK adds a ton. [0] I should note that SPARK 2014 is also available as a GPL'd "community" edition. EDIT: Asterisk + HN formatting