Not to mention the changes to the SPARK subset of Ada for doing proofs on parts of your code have improved a lot.