> industry baremetal profiles like Ravenscar I understand the value proposition of Formal Verification with Spark. But for me the killer features with Ada, th

> industry baremetal profiles like Ravenscar I understand the value proposition of Formal Verification with Spark. But for me the killer features with Ada, thinking specifically of embedded systems is: - The expressiveness you gain with Ada's Type System - The Ravenscar profile (very impressive work from a small group of folks in the IRTAW group)