大学でRustを教えた話
このブログ記事は、Advent Calender 2020, Rust 3、23日目の記事となります。自分は現在大学で教員をしていまして、セキュリティ系の研究室に所属しています。現在はセキュリティの講義を担当しており、そこでRust言語を教えているため、その内容を紹介しようと思います。
はじめに
皆さんご存知のようにソフトウェアの脆弱性は今でも大きな問題となっていますが、それを完全ではないにしろ根本から解決するための技術的手法として型システムが注目されています。型システムの考え自体は古くからありますが、最近ではRust言語が登場し、OSなどいわゆる低レイヤーなソフトウェアも型システムの恩恵を預かることができるようになってきました。SMTソルバや定理証明などと言った難しい（かつ面白い）手法でC言語やC++言語で書かれたソフトウェアを解析する方法もありますが、セキュアソフトウェアを語る上では、現在では、まず型安全なプログラミング言語を利用するのが先決だという信念から、セキュリティの講義でRust言語を教えました。
講義の受講者は、大阪大学、京都大学、北陸先端科学技術大学院大学、奈良先端科学技術大学院大学らの大学院生と社会人学生となっており、基本的に情報系の大学院生と社会人を対象としています。大学院の講義なので、単なるHow toを教えるのではなく、Rust言語の裏側にある理論的背景から説明するように心がけました。逆にいうと、理論的なことは教えるのですが、データコンテナやCargoなどの使い方は自習が求められる構成となっているため、ある程度は自分で調べる必要があります。
講義の内容
Rustに関する講義は以下の通りとなっています。いずれも1回90分の講義となっています。
- ソフトウェア技術についての概要説明（GC、型システム、様々なバグ）
- Rust言語について
- 線形論理と線形型システム
- 線形型システムの実装
- 並行プログラミングとRust
ソフトウェア技術について
まずはじめに、ソフトウェアとソフトウェアテストに関する技術について概要を説明し、以降で説明するRust言語についての立ち位置を明確にするように心がけました。この文章を読んでいる方はRust言語の存在は当たり前に知っているとは思いますが、Rust言語はまだまだマイナーな言語で、その存在すら知らなかったという学生や社会人の方も多くいらっしゃいました。その中で、他にもいろいろなプログラミング言語があるのに、何故Rustというマイナー言語を新たに学ぶ必要があるのかという手厳しい質問も頂戴しました。
これは難しい質問で、確かに、他にもOCamlやHaskellと言った先駆者があり、それら言語であればRustの借用と言った複雑な機能に煩わされることも無いのは確かです（Haskellのモナドが借用より簡単かと言えば難しいところですが）。ですが、現状の流れを見ると、OCamlやHaskellが主流になることはしばらくは無さそうですが、RustがCやC++の代替となる可能性は十分にあり得ます。ICTインフラがますます普及し、ソフトウェアが我々の命までも支えるようになってきた昨今では、C、C++をRust等のメモリ安全な言語で置き換えることは、ソフトウェア業界の最重要課題と言っても過言ではありません。このような状況を鑑み、本講義ではRust言語を選択しました。
Rust言語の説明
ソフトウェア技術の概要を説明した後は、Rust言語についてざっと説明しました。この回で基本的な構文や、借用について説明し、コンパイルの仕方も簡単に説明しました。2回目の講義レポートでは、AArch64アセンブリの簡易版エミュレータをRust言語で実装してもらいました。簡易版ですので、命令セットは四則演算と、条件分岐だけという簡素なものですが、この課題でenum型やパターンマッチ、moveセマンティクスなどの諸概念について体感してもらいます。
実際のレポート課題としては、以下のようなアセンブリファイルを読み込んで実行するようなものとなります。エミュレータと言っても、機械語ではなくアセンブリ言語をそのまま解釈するためスクリプト言語処理系と言った方が正確かもしれません。
線形型システム
次に、線形型システムについて説明しました。ここでは、Rust言語の理論的背景的にある線形型システムについて（実際はアフィン型ですが）、線形型言語をもとに説明しました。内容的にはATTaPL (*1) の線形型言語にいくつか改良を行ったものを用いました。型付け規則から説明して、型付け規則を用いた証明まで行うため、何故Rust言語でuse after freeやdouble freeが防げるのかを、理論的な側面から理解できるようになります。
この講義のレポートでは、次のような型付けに関する証明を行ってもらいましたが、多くの学生がしっかりと証明できていました。正直、ATTaPLを独習して証明までできるようになる人は多くはいないと思うのですが、本講義を90分受講して課題にとりくむと証明できるようになっていますので、これは凄いことだと思います。
その後、線形型言語の型検査アルゴリズムを、Rustを用いて実装してもらいました。アフィン型の言語であるRustを用いて、線形型システムを実装することで、Rust言語自体がよりよくわかるようになるという寸法です。この講義よりも前に初学者にRust言語を教えたことがあるのですが、moveセマンティクスの理解に時間がかかるようでしたが、これら課題を行うと完璧に理解できます。
(*1) ATTaPL: Advanced Topics in Types and Programming Language
並行プログラミング
この講義はつい先ほど行ったものですが、ここではRustでの並行プログラミングについて説明しました。Rustは並行プログラミングについても非常によく設計されております。その実現には、借用とトレイト制約が重要な役割を果たしていますが、それらについて講義をしました。ここではRustだけではなく、クリティカルセクションやレースコンディションなどの一般的な諸概念と、アトミック命令を用いたスピンロックアルゴリズムの紹介も行います。この回でRustに関する講義は終わりになるのですが、続く回ではモデル検査機のAlloyを用いてスピンロックやRWロックアルゴリズムの検証を行っていく予定です。
以上が講義の内容となります。回数自体は多くありませんが、Rustの基礎的なところや何故Rustなのかぐらいは分かる内容ではと思います。
まとめ
本講義ではRust言語とその理論的背景となる型システムまで教えましたが、自分はプログラミング言語理論は専門ではなく、どちらかというと、OSやネットワークなどのシステムソフトウェア、並行プログラミングの実装などが専門となります。そのため、線形型などの理論をどう教えたものかと大変悩みましたが、結果的には理論と実装をバランス良く扱うことができたかなと思います。本当はOSやネットワークスタックをRustで実装するような内容にしたいのですが、しょうがありません。
世間では、「大学では古い技術しか教えていない。トヨタなどで使っている最新鋭の技術を教えるべきだ」、などと言ったご意見もありますが、本講義のように、トヨタでも少数の人しか使っていないであろう、そこそこ最新の技術も多少は教えられているのではと思います。
それでは皆さん、メリークリスマス。
