Rustのコードチェックを強力にする3つのツール | κeenのHappy Hacκing Blog
κeenです。 Rustaceanのみなさんは普段書いてるRustのコードを検証するのに cargo check や cargo test などのツールを使っているかと思いますが、それらを強力にするツールの miri 、 MIRAI 、 kani をそれぞれ紹介します。 Rustにはいくつかコードの正しさや行儀のよさを検査する方法がありますね。 cargo check や cargo test 、 あるいはビルドしたバイナリを走らせて検証したり色々手を尽くしているでしょう。 ですがこれらだけだとあらゆる種類のバグを拾いきれる訳ではないのもみなさん承知の通りだと思います。 既存の方法だと手が回らない所があるので他のアプローチでコードを検証してくれるツールがあると嬉しいですよね。 そういったツールを3つ紹介します。 先に注意しておくと、これらのツールはまだ成熟しきってはおらず使いづらい点、使い
高精度に漢字変換できるSKK辞書を作った（四角号碼、正假名） | κeenのHappy Hacκing Blog
κeenです。漢字変換高精度に行うためにSKK辞書をいくつか作ったので報告です。 辞書 GitHubに上げています。手元にダウンロードして各々好きなように使って下さい。ライセンスはCC BY-SA 3.0です。 SKK_JISYO.wiktionary 解決したい問題と対応する辞書 SKKに限らずほとんどの日本語での漢字変換は読みを入力してそれに該当する候補から漢字を選択していると思います。この方法は直感的で分かりやすいのですが、私は2つ問題を感じています。 同じ読みに対する候補が多すぎる 読みが分からない漢字を変換できない 1の候補の数については特に音読の入力に対して顕著です。例えば「しょう」で変換するとSKK_JISYO.Lにある候補は174あり、その中から目的の漢字を目grepで探す作業がはじまります。変換したい漢字は思い浮かんでいるはずなので、この目grepはインタフェースが洗練さ
ウワサのVeronaを眺めてみる | κeenのHappy Hacκing Blog
κeenです。 先日、Microsoft Research (MSR)からVeronaという言語が公開されました。 マイクロソフト、Rustベースのセキュアなプログラミング言語を探求中 - ZDNet Japan マイクロソフト、「Rust」に基づくプログラミング言語プロジェクト「Project Verona」がGitHubに - ZDNet Japan これを見た人達の反応が様々で（婉曲表現）面白いな（婉曲表現）ーと思いました。 最近は企業や大きな団体の作った言語がメインストリームで使われることも増えたことから、本来の目的以上に期待を背負ってしまった感じがします。 プログラミング言語は思ったよりも気軽に作られているものです。 例えばGoogleの開発したohmuという言語はほとんど誰も知りませんよね。 そういうもんです。 以下には私がドキュメントとかコードとか読んだ感想を書きます。 主に
JITあれこれ | κeenのHappy Hacκing Blog
κeenです。遅刻してしまいましたがこのエントリーは 言語実装 Advent Calendar 2018 1日目の記事です。 最近私の観測範囲内でJITが流行っているのですが一口にJITと言っても色々あるよなーと思ったので私がJITについて知っていることをグダクダ話します。 このブログでも何度がJITや周辺技術について取り上げてますが話の流れがスムーズになるので最初から説明していきます。 2018-12-03: 加筆修正しました。差分はこちら JITって？ Just in Time(コンパイル)のことで、日本語にすると「間に合ってコンパイル」になりますかね。 インタプリタの高速化テクニックの1つです。 最初はインタプリタのようにコードをコンパイルせずプロセスが起動しますが、メソッドを実行するまでにはメソッドをコンパイルして、ネイティブコードで実行する方式です。 本来ならJITはこのような意
自然言語のアウトプットを継続的に出すためには | κeenのHappy Hacκing Blog
κeenです。ミスってコーヒーと濃いめの緑茶を喫してしまって眠れないのて一筆執ります。 ふとソフトウェア界を見渡すにブログやドキュメントなどを継続的に書いてる人って意外と少ないのかなと思ったので自分なりに続く方法を書いてみます。 下記が統計コマンドと結果です。2018年はまだ3ヶ月弱残ってる上にアドベントカレンダーがまだなのでもう少し伸びる可能性がありますがまあ、+10程度でしょう。 $ find content/post -type f | xargs grep -h date: | grep -o -E '[0-9]{4}-[0-9]{2}-[0-9]{2}' | grep -o -E '[0-9]{4}' | sort | uniq -c 24 2013 39 2014 52 2015 48 2016 32 2017 25 2018 $ find content/slide -typ
isucon7予選のアプリをRustに移植したから解説するね | κeenのHappy Hacκing Blog
κeenです。こういう流れがあったので移植しました。 keenさんが「2028年、Rust でイケてる web application framework はこれだ！」みたいな記事を書くとと "余力" が生まれるかもしれません…！！ — FUJI Goro (@__gfx__) 2018年8月28日 まずISUCONを知らない方に雑に説明しておくと、意図的に遅く作られたWebアプリケーションが与えられるので7時間くらいでどれくらい高速化できるかを競うコンテストです。 このお題のWebアプリケーションが参加者や流行りに合わせて複数言語で提供されるのですが、今年はRustが来そうだということで参加者の肩慣らしのために過去問を移植しましたというお話。 ひとまずソースコードは こちら 手元でベンチマークをしてみた限り、Pythonの2倍くらいは速いもののGoには劣るようでした。これの考察については
ATS2の依存型を使ってAVL木 | κeenのHappy Hacκing Blog
κeenです。少しばかりATS2を触ってみたので成果報告でも。 AVL木は左右のノードの高さが高々1しか違わない平衡二分木です。OCamlやSMLでナイーブに実装すると本当に1しか違わないことを保証するのは難しく、精々テストなどで部分的に検査するだけです。 ところがSMLに似た文法を持つATS2には依存型があり、左右のノードの高さが高々1しか違わないことを型で保証出来ます。 つまり、左右のノードの高さが2以上違う木を作ろうとしてもコンパイルエラーになるのでコンパイルが通れば高さについてはバグがないこと保証されます。 そういうAVL木を使ってTreeSetを作ってみたので紹介します。 私のブログ(のこの記事)の読者ならATS2も依存型もAVL木も知ってそうですが一応説明します。 ATS2って何? 詳しい説明は日本ATSユーザグループに譲るとして、この記事にて重要な点を挙げます。 SMLに似た
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
静的なメモリ管理の話。リージョン推論とλ計算からRustまで | κeenのHappy Hacκing Blog