Considering Avionics domain, using Coq or ATS to prove the correctness of SolScript compiler will help boost confidence.