Scribble at 2025-02-14 10:50:36 Last modified: unmodified

SPARK というのは、形式証明された厳格なシンタクスをもつ Ada という言語のサブセットとして開発されたプログラミング言語だ。テスト・ケースを作って大量に試行を繰り返すような帰納的アプローチとは違って、形式的に安全と定義された条件でコードの妥当性を証明するという演繹的アプローチを採用していて、精密かつ安全な設計が求められる分野での採用事例が多い。宇宙工学や自動車の運用機器、それから NVIDIA でも採用されているという。ただし、SPARK の元になっている Ada という言語は非常に精密な文法を持っていて、多くのプログラマから複雑さを嫌われている C++ ですら足元にも及ばないほど難しいと言われているので、当然のようにサブセットの SPARK についても一般向けのリソースは殆どない。たとえば、Brainfuck のような実用性がない言語のエントリーすらあるウィキペディア（日本語版）のエントリーもないし、書籍を探しても検索して出てくるのは、たいてい名前が似ている Apache Spark のものだけだ。なので、上記のサイト（開発元の一つである AdaCore）くらいしかまともなリソースがない。