What is it about ada which makes it particularly useful for this purpose? Can the Julia language inherit those features too in the long run? Another formalistic language I want Julia to learn from is agda.
Programming in pure type theory involves a lot of tedious and repetitive proofs, and Agda has no support for tactics. Instead, Agda has support for automation via reflection. The reflection mechanism allows one to quote program fragments into – or unquote them from – the abstract syntax tree. The way reflection is used is similar to the way Template Haskell works.[8]
Reflection is also what Julia metaprogramming is based on, so extend the type system of Julia?