Ada 言語や SPARK 言語は，長く航空宇宙分野で用いられてきました．Ada は強い型付けを特徴とし，SPARKは，述語論理を用いた記述や形式検証をサポートします．
現在では，コミュニティ版があり，誰もが簡単に言語を試すことができるようになっています．最近では，Web上での学習用サイトも充実しています．今回このコミュニティ版を用いて，Micro:bitでのプログラミングをご紹介したいと思います．簡単に楽しく言語を学ぶことができることと思います．
https://ada.jp/?p=46