Kotaro Chikuba mizchi

Using Lean as an Executable Test Oracle

Summary

Lean is useful even when you do not verify the implementation itself. You can encode a specification as a small executable model, generate a test corpus from that model, feed the same inputs to a real checker, compiler, or runtime, and report disagreements as counterexamples.

The essential separation is:

Correctness inside the model: Lean checks the semantic decision procedure and its theorems.
Correspondence with the implementation: an external adapter runs the implementation and compares its observations with Lean's decisions.

SIMD Lexer Pipelines: Classify, Carve, Coalesce, Compress

I prototyped a v128-based lexer optimization using the JSON parser in moonbitlang/core as the target. This note distills the design into a SIMD lexer pipeline that can be applied to JSON, JavaScript, and other languages.

The short version is that bitmasks are indeed the key abstraction. However, the main opportunity is not matching CST node kinds after construction. It is classifying input bytes and extracting only the positions where lexical context can change.

The pipeline

A typical pipeline can be decomposed as follows:

pkg	dir	direct_runtime_dependents	transitive_runtime_dependents	test_dependents	runtime_imports	usage_non_test	usage_total	loc	score
moonbitlang/core/builtin	builtin	74	74	0	1	19391	63750	17038	619.11
moonbitlang/core/debug	debug	45	56	9	8	351	5463	1769	401.12
moonbitlang/core/float	float	8	57	3	3	679	1934	277	221.31
moonbitlang/core/array	array	23	42	7	1	0	5	10	202.58
moonbitlang/core/double	double	8	58	4	1	53	873	59	201.46
moonbitlang/core/quickcheck	quickcheck	17	32	4	4	26	201	118	185.98
moonbitlang/core/int16	int16	7	59	1	1	15	212	95	185.90
moonbitlang/core/abort	abort	1	75	0	0	1	3	13	163.32
moonbitlang/core/test	test	14	38	34	2	0	2984	134	162.00

実装コードから仕様を吸い出して Z3 / TLA+ でバグを払い出す — 実践プレイブック

既存システムの実装を「事実上の仕様」とみなし、それを形式化することで「テストでは踏めないバグ」と「実装が暗黙に決めている仕様」を炙り出すための手順書。仕様書が無い / あてにならない / 仕様と実装がずれている、という現場を前提にする。

0. 基本姿勢: コードが de-facto 仕様である

現状の分析

AI、全方位にレバレッジが効くからやらない理由がない
AIが書き、AIが読む
人間はAIを通して要約を読む(だけ)

今、書くことなくない？

GA みたいに、ブラウザに公開キーを埋め込んでイベントを送るサービスを考える。

公開キーは secret ではない。script tag や bundle に入るので、誰でも見える。ただしサーバー側では、その公開キーから token record を引いて、project と origin allowlist を見る。

このとき落とし穴になるのが domain verification。

「この origin はこの project のものだ」と確認できていることと、「この origin から telemetry を write してよい」ことは別の権限になる。

name	gleam-practice
description	Best practices for building and reviewing Gleam projects on the Erlang target, especially Wisp plus Mist web services, OTP processes, justfile workflows, testing, formatting, CI, and performance measurement.

(LLMに gleam を書かせながら生成した SKILL.md)

Gleam Practice

Gleam を新規作成するとき、既存プロジェクトを改善するとき、wisp + mist + gleam_otp + just 構成で実装するときに使う。

v-tokyo24 発表資料の原稿. スライド版はあとで公開。

(このままのが読みやすいかも)

	[package]
	name = "cognitive-rhythm-eval"
	version = "0.1.0"
	edition = "2024"
	rust-version = "1.85"
	description = "A measurable proxy evaluator for Japanese cognitive writing rhythm"
	license = "MIT"

	[dependencies]
	encoding_rs = "0.8"

	#!/usr/bin/env bash
	set -euo pipefail

	NIX_VERSION="2.24.9"
	export USER="${USER:-$(id -un)}"
	export HOME="${HOME:-/root}"

	# nix.conf を先に置く (sandbox 無効・flakes 有効)
	mkdir -p /etc/nix "$HOME/.config/nix"
	cat > /etc/nix/nix.conf <<'EOF'