Ada as an ecosystem has it's own alternative, SPARK. It's not a dependently typed language, but you can go just as far with it using pre and post conditions, an

Ada as an ecosystem has it's own alternative, SPARK. It's not a dependently typed language, but you can go just as far with it using pre and post conditions, and ghost code, insofar as what you can prove. You can see here for more information: http://www.spark-2014.org/ http://www.spark-2014.org/ http://docs.adacore.com/spark2014-docs/html/ug/en/tutorial.html http://docs.adacore.com/spark2014-docs/html/ug/en/tutorial.h...