読者です 読者をやめる 読者になる 読者になる

mixiにMizarのコミュニティが作成される

久しぶりにMixiにアクセスして、足跡を見て、ある一人のかたの所属するコミュニティを
確認してみると、Mizarなんてものがあった。

これはもう、私が入らせてもらっている、SUGSIのコミュニティからやってきたに違いがないと考えて、
SUGSIコミュニティへとぼうと思ったが、よくみてみるとMizarコミュニティというものが。

どうやら管理人は、しろだぬきと書いてあるので、わかる人にはわかると思う。
開始日は3月14日から・・かぁ。

個人的にMizarというプログラム言語はどうしても好きになれない。
Mizarという言語はいわゆるプルーフチェッカだと、N村先生のサイトに書いてあったけれども、
どうも雰囲気がFortranCOBOLの悪いところ(いや、個人的な感想です。)を集めたような印象があるのである。
Mizar言語についてはここを参照

COBOLについてはここを参照

かいつまんでいえば、

である。
つまり、Fortranはコメントを付けるときは、一文字目に``C''をつけなければならない
といった、こうせねばならない的記述が多かったり。
数学者ならばすんなり Mizar 論文を読んで理解することが可能である
とかである。

もう少し自由度が欲しいのである。
しかし、自由であれば自由であるほど、どのようにでもかけてしまうので、
数学者ならばすんなり Mizar 論文を読んで理解することが可能であることにはならないけれども。

なんというか、記述形式が古臭く感じてしまうのだ。それが悪いという気持ちはまったくない。
古いほうが過去の資産があるという点でGoodなのである。ただ、なんとなく、C++Javaで育った
私としては、オブジェクト指向とまでは言わないが、もう少し自由度をあげて欲しいなぁ。と思うわけである。

昔、素粒子実験の研究室にいたときも、C++言語がベースな、ROOT言語というものが存在して、今も使っている言語である。
解析に最適。しかし、FortranがベースであったPAW言語の方がよくつかっていた。今年の教育論文では、
PAW言語とROOT言語の両方を使ったが、去年まではすべてPAW言語しか使っていないくらいである。

それはなぜかというとPAW言語は結局ごちゃごちゃして可読性に劣るがROOT言語よりも、
おおくの先輩方の資産や、自分のライブラリがあるから、なかなか移行しにくいのである。

そろそろ眠い。結論を言おう。
Mizar2が出るのをちょっと期待しているのである。私はMizarを全く使いたいと思わないが、
簡単なプルーフチェッカなら欲しいのである。本当に単なる論理演算用途として。電子回路製作に使えそうなのだ。
しかし、今のフォーマットはどうしても好きになれないので、オブジェクト指向系のMizar2とかでないかなぁ。

素粒子実験のときは、Geant3(Fortranベース)がGeant4になると、C++形式となり、完全なオブジェクト指向言語になった。
こんな風になることを切に望むのである。まったく私のわがままですが。
http://www.nuclear.phys.tohoku.ac.jp/~kazunori/G4Lec01/sld001.htm