芳賀 雅樹 / Masaki Haga

@silasolla

About Me

ソフトウェアエンジニアとして,アプリケーションの開発や,開発プロセスの内製化支援のお仕事をしています. アプリケーションのコーディングからパブリッククラウドまで,なんでも幅広くやっています. 最近は DevOps の実践に関心があります.

技術やツールのブラックボックスになっている部分,それらを裏付ける理論計算機科学や数理論理学,関数型プログラミングなどにも興味があります. お気に入りのプログラミング言語は Standard ML です.(流行りの Machine Learning ではなく Meta Language です.)

人 (開発者にもユーザにも) に優しいプログラミング言語やツールと,それらを醸成してきた人々を尊敬しており,今後の普及や発展に貢献できたらなと思っています. コミュニティや OSS などに支えられながらの日々ですが,これまで享受してきたぶん,自分も還元していけたらなというのが目標です.

Experience

2025年6月 - 現在

株式会社スリーシェイク - Sreake 事業部

アプリケーション開発支援チーム (Full Stack)

アプリケーションの開発やクラウドネイティブな開発プロセスの内製化支援をやっています.

2022年4月 - 2025年5月

株式会社ソニックムーブ - 開発部 (Solution 事業)

ソフトウェアエンジニア (Web Backend / Public Cloud)

Web アプリケーションの受託開発やレガシーなシステムのリプレイスなどをやっていました.

Education

2020年4月 - 2022年3月

新潟大学 大学院 自然科学研究科 電気情報工学専攻 情報工学コース

修士 (工学)

プログラミング言語の基礎理論の研究をしており「項書き換えシステム」という計算モデルの性質を調べていました.

2016年4月 - 2020年3月

新潟大学 工学部 情報工学科

学士 (工学)

学生として情報工学を体系的に学んでいました.プログラムを書くことだけでなくコンピュータの仕組みを知ることが好きでした.

2013年4月 - 2016年3月

福島県立安積高等学校 普通科

Publications

2022年3月

修士論文:置換に関する不動点制約を用いた名目書き換え

詳細を見る

名目書き換えシステム (Nominal Rewriting System) という計算モデルの性質について. PPL 2022 (第24回プログラミングおよびプログラミング言語ワークショップ) でも発表しました.

リンクを開く

Certifications

Misc

Notes

構成的に証明できないトートロジー
詳細を見る

トートロジーの自然演繹体系での証明木集です. 背理法や二重否定の除去などを使わないと証明できない (証明は省略) ものを扱っています.

リンクを開く
様相論理の体系と Lindenbaum の補題
詳細を見る

様相論理の体系の定義から始まって Lindenbaum の補題を導きます. 様相論理と言いつつ極大理論を作る話がメインです.

リンクを開く

Tools

Bluesky の投稿を消すやつ
詳細を見る

自分の発言を削除して責任逃れをするための簡単な Python スクリプト. GitHub Actions で Workflow を動かして定期実行できます.

リンクを開く
退職届を作るやつ
詳細を見る

退職届 (PDF) を作るための LuaLaTeX コードスニペットです.

リンクを開く
項書き換え系を完備化するやつ
詳細を見る

Standard ML で書いた一階項書き換え系を操作する UNIX コマンドです. MLton でコンパイルします.

リンクを開く
証明写真のリストを作るやつ
詳細を見る

写真データを縮小して PDF ファイルに並べます. コンビニプリントして切り取ることで印刷代をケチることができます.

リンクを開く
Brainf*ck のインタプリタ
詳細を見る

すべての人類が一生に一度は書くことで知られるインタプリタです. Standard ML で書いてます.

リンクを開く
担々麺屋
詳細を見る

担々麺屋に行きたくなるページです. Matrix Canvas Code (https://gigazine.net/news/20130321-matrix-javascript/) を真似しました.

リンクを開く

Hobby

Standard ML

ゆるく関数型.操作的意味論すごい! HM 型推論すごい!手続き型との良いとこ取りすごい! SML# 頑張れ!

Haskell

はじめて関数型プログラミングするときに触った.遅延評価!お仕事で使うのがあこがれ.

Elm

コンパイルエラーが丁寧ですごい!ゴリゴリ書かなきゃなスタイル.

Racket

Scheme! Homoiconicity! call/cc! shift/reset!

Koka

代数的エフェクトの.勉強中!

型システム

推論が柔軟に動くレベルのと依存型くらい表現力強いのを適材適所で.

定理証明支援系

Isabelle/HOL の本読んでた.Lean, Agda, Idris など勉強中.

音楽

クラシックや現代音楽から世界の民謡やロックバンドまで幅広く聴きます.

クラシック音楽

Alkan, Liszt, Brahms, Bruckner, Franck, Sibelius, Webern, Varèse, Messiaen, Xenakis, Penderecki, Crumb, 諸井三郎, 湯浅譲二あたりが好きです.

King Gnu

どのアルバムも何周したかわからんくらい聴きました.Millennium Parade も好きです.常田大希さんリスペクトです.

Tuba

中学校から大学までやっていました.デカすぎて個人所有が厳しいですがベースラインに耳が行きがち.

ピアノ

母が実家でピアノ教室やってたので帰省したときに練習してます.ガチ勢じゃないのであんまり.

数学

計算より証明を追うのが好き.数理論理学に一番興味ありますが,メタじゃないのもやります.

国内旅行

知らない景色や根付いた文化を見に行くのが好きです.最近は静岡県 (熱海, 初島, 沼津, 三島, 三保松原, 三島, 天竜二俣など) を攻めてます.

散歩

街並みを見ながら尋常じゃないくらい歩きます.2日で 42.195 × 2 km 歩いたり,浅草から新宿まで歩いたりもします.

日本庭園

四季折々の景観が楽しいです.草花や野鳥を眺めながら,のんびりと歩いています.浜離宮恩賜庭園の年パス持ってる.

読書

コンピュータや数学などの理工書がメインですが,藤子F不二雄のSF短篇集や謎雑学本もよく読みます.最近は柞刈湯葉さんとか.

けろけろけろっぴ

サンリオ人気投票で毎年投票してます (有象無象に負けるな).部屋のカーテンも文房具もよく使う LINE スタンプも全部けろっぴです.

科博

特別展に毎回行っています.いつも展示のボリュームが凄くて,たくさん新しいこと知れたなって満足してます.

神保町のカレー

最近は共栄堂のスマトラカレーにハマってます.疲れているときに食べるとありえん美味い.

トマトジュース

塩分が無添加のやつ.

旅行で海の近くに行ったときに食べるお刺身ほど美味いものはない.

天麩羅

目の前で揚げてもらったやつありえん美味い.

ラーメン

あっさり系のシンプル醤油ラーメンが好き.

ビール

天然素材でこんなに金色の液体ってあるだろうか.神に祝福されている.クラフトビールやビアカクテルも.(not 任意の酒)

甘いもの

すきだけどおでぶに.

カフェ通い

カフェ「巡り」ではない.お気に入りのお店にたくさん行きます.

ごちうさ

救われました.

ゆるキャン△

おもしろい.実写も良かった.

まどマギ

脚本とキャラデザと音楽と演出と総合芸術.

ドラえもん

大長編ドラえもん全部持っている.映画も映画館で見ていた.

ゲーム

シナリオやゲームシステムや音楽に引き込まれる.好きなゲームはサルゲッチュ,ロマサガ,オクトラ,ドラクエ7,深夜廻など.

言葉遊び

自己言及文,部分文字列,回文,駄洒落,(何のとは言わないけれど) 語録遊びなど.

自分

他人に優しく,自分には更に優しい.