This is a real life story of a mixed criticality system, where a proper usage of Ada's features for controlling visibility allowed a provable enforcement of the segregation rules at compile time: any violation would simply not compile.
Speakers: Jean-Pierre Rosen