Skip to content
View zzjrabbit's full-sized avatar
☹️
Doing homework.
☹️
Doing homework.

Block or report zzjrabbit

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Content in all repositories owned by your account will be closed.
Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
zzjrabbit/README.md

zzjrabbit

Start from the unreachable. Reach for the unknown.

zzjrabbit.github.io

I build things to understand how they work. Languages, kernels, proofs, and the machinery in between — I would rather take an abstraction apart and rebuild it than take it on faith.

Principles

KISS. Keep it simple. A small kernel with clear rules beats a large system with unclear ones, and most complexity is a decision nobody went back to question.

First principles. Learn from the inside out. When something becomes interesting enough, implement it, break it, or state its assumptions precisely enough to be checked.

Observable machinery. Hidden state should stay inspectable; a design that cannot be seen is a design that cannot be fixed.

Finish the experiment. Even an unfinished project should leave behind something that teaches.

Tools

Rust is where most of the work happens. Lean when a claim deserves a proof, Typst when an idea deserves an explanation, Nix when an environment deserves to be reproducible, C and assembly when the machine itself is the point.

Currently

Reading more mathematics, formalizing the parts worth keeping in Lean, and poking at the boundary between languages, systems, and logic.

Pinned Loading

  1. ligare-lang/ligare ligare-lang/ligare Public

    A simple DTT like programming language.

    Rust 1