#はじめに
世の中にはいろいろなプログラマがいるし、プログラマが使うプログラミング言語も同じく多く存在する。C#は神の言語だという人やRustの更新情報をいつもチェックしている人など、周りを見るとプログラミング言語宗教に染まってしまった人は結構いるはずだ。しかし、プロジェクトが変われば使う言語も変わるし、いろいろな言語を知っていることは損ではない。そんな中、言語を探していく内によく分からないし使い方も分からない言語を見つけることもあるはずだ。その言語に触れていく内に芽生える恋にも似た偏執を感じたら最後。それはさながら、映画鑑賞が趣味の人間がA級からB級に堕ち、5分以内にサメかゾンビが出てこないと満足できない身体になるように戻れなくなってしまう。そう、私のように。というわけで、人が知らないような言語を紹介してみようと思う。それは、開発段階かもしれないし、開発が終わった言語かもしれない。ここでは、それらをB級言語と呼ぼうと思う。そして願わくば、それらがA級言語と呼ばれるようになった時に、最初はこうだったのにと思えると面白いかもしれない。
#Fって何よ？
タイトルにもあるが今回はF(Fスター)を紹介しようと思う。感のいい人はタイトルで気づいただろうが関数型言語だ。そして、Micro SoftのF#なら知ってるという人がほとんどだろうと思う。現に、「F* programming」と検索してもトップはF#になってしまうことがある。なんてことだ！ちなみにF#について知りたければ「F# を知ってほしい」を見るといい。ついでだが、この記事ではF#とFを詳しく比べる気はまったく無い。ジョーズとB級サメ映画を比較しても虚しくなるだけといえば分かるだろう。それでは本題に戻そう。FはF#と同じMicrosoft Researchで開発されている。現状では、F*単体では実行はできないが、プログラムを検証し、OCamlやF#にエクストラクトして、その言語のコンパイラによってコンパイルすることで実行を行うことになる。ここで重要となるのは検証を行うことである。話が長くなりそうなのでこれは次のセクションに持ち越そう。
#プログラムの検証
さて、サイトの翻訳に従えば「検証」というワードを使っているが、「証明」といった方が分かりやすいかもしれない。既にCoqやAgdaやといった証明支援システムを知っているならなお良い。本題だが、プログラムの品質保証行う上で、「プログラムが正しい」とはどう言えるのだろう。例えば、「この関数は返り値をNULLとしない」、「このリストは常に3番目を参照できる(リスト長が3以上)」とはどう言えばいいだろうか。まぁ、この程度であれば数回テストをすれば問題なさそうだが、もっと難しい問題となった場合はという話だ。ここで、定理証明支援というものが登場する。難しいことは言わないし、そもそもこの分野は難しすぎて私の口からおいそれと言えないのだが、定理証明では、普遍的な諸々の性質から結論に得ることでプログラムの正しさを導き出す。つまり、これを半自動的にやってくれるのがFで、大雑把に言えばF#にCoqを足したらFになったようなものだろう。
#環境を作る※必要なら
環境を作るのは簡単だ。ホームページから自分のOSに合ったバイナリをダウンロードしてパスを通せばいい。そう、F単体の環境を作るのは簡単だ。だが、前述したようにFは単体では実行できないため、F#やOCamlにエクストラクトしてから実行する必要がある。Windowsを使っていてOCamlの環境を作ろうなんてするのは骨が折れる。Visual Studioを使ってF#の環境を整えるのがいいだろう。もし、環境を作りたくないというなら、online F* editorを使うといい。解説もあるし、私がいちいちコードを書いて解説する必要もなくなる。
#最後に
雑な記事書いてごめんなさい。
#参考
F*: A Higher-Order Effectful Language Designed for Program Verification
F - Metasepi