>There is no magic in Ada, Oracle, etc.
There is no magic but there are strong constraints that shift reliance for correctness from fallible human programmers and peripheral tools to the type system and compiler, providing better integrated, systematic assurance.