こんにちは
F# のアドベントカレンダーの記事ということで、F# の話題を楽しみにされた方々には申し訳ないのですが、この記事では F* というプログラミング言語を紹介します。F* は「えふすたー」と読みます。
公式サイトは以下になります。
なんだか論文とかおいてあってやたらハイソな感じがしますね。それもそのはず、開発にはマイクロソフトリサーチが関わっています。
いったんここで「なぜ F* を取り上げたのか？」について説明しないとそろそろ F# の記事を期待されている方たちから石が投げられそうな気がしますので説明させていただきますと、基本的には F* は F# とよく似た言語ですし、なんと F で書いたプログラムは F# に変換することができる1のです！*
言ってみればマイクロソフトの尖った野郎ども2が作ったイケてる Alt F# なんですよ。
メインの領域としては定理証明などを想定しているみたいです。Agda とか Coq みたいなのに近いんですかね。
ここで F* の驚きのコードを…紹介できればよかったんですが、じつは私、これ書けないんですよ！！！
でも、論文(PDF)がなんかヤバくって
うわー、なんかすごいことができそう。
読んでもぜんぜん分かりません！
はいー、心折れました。
ポキリンコッ！！！
そんなわけで、お客様の方々におかれましては F# に詳しい方もいらっしゃるでしょうから、ぜひこの言語を使ってみて、素晴らしさを私に教えて下さい。
どうぞよろしくお願いします！
うわー、石投げないでおくれぇ〜
-
なんか他にも最適化のためにC言語のコードに変換できたりもするみたい ↩
-
マイクロソフトリサーチ以外にも MIT や INRIA みたいな大学からのコミットも多いみたいです ↩