2022年抱負

κeenです。2021注目していきたい技術、やっていきたいことを書いておく。 Axum Rustの新しいウェブアプリケーションフレームワーク。Toki

2021年振り返り

κeenです。まだ大掃除終わってないけどこれ書かないと一年が締まらないので筆を執ります。

RustでDockerの--passwordで入力したパスワードを盗む

このエントリはRust Advent Calendarの9日目の記事です。

空いてる日を埋める担当のκeenです。9日目が空いてたので遡って記事を投稿します。RustというよりLinuxの知識を使った記事ですが。Docker CLIでログインするときに --password オプションを使うとパスワードが盗まれる可能性があるよという警告が出たことありませんか?あれを実際にやってみたいと思います。

SML#のexistential typeで遊ぶ

κeenです。SML# 3.7.0から実験的機能として _dynamiccase に存在型のサポートが入ったので試してみます。 本記事はSML# 4.0.0 with LLVM 12.0.0で動作確

Idris 2の数量的型が解決した問題、導入した問題

関数型言語Idrisの次世代版として開発されているIdris 2の大きな特徴の1つとして型システムに数量的型理論(Quantitative Type Theory)を導入していることが挙げられます。このシステムではIdris 1にあった証明環境での利用可能な値の問題や、本来ならば実行時に不要な型を持ってしまっていた問題を解決します。一方で数量的型を便利に使うための仕組みであった多重度の部分型付けにより非健全性が入るなどの問題もありました。本発表ではIdris 2の数量的型のそういった特徴を紹介します。