Inside digitdisk: 2,206 lines of flang decide, 20,678 lines of Go act

digitdisk is a tool that shows where the disk space went and, on command, clears the surplus away. It is written in two languages: flang — a language where a function carries postconditions and the compiler checks them — and Go, the one that talks to the operating system. What the tool does has a page of its own; this piece is about how it is built inside: where the boundary between the two languages runs, who is allowed to say “this file may go”, and why the screen is not given that right even when a person presses Backspace.

It is worth reading for one reason: the boundary here is drawn not along application layers and not along packages, but along the kind of statement. Everything that can be proved lives in one language; everything that can only be done lives in the other. Below you can see what that cost and what was left outside. Every number names the command that prints it — all of them can be repeated in any clone.

Five answers up front

In one line, if there is no time for the rest: a new rule is an edit to the flang core and its proofs, not an edit to a Go command. The whole build of the tool is arranged to make going around that inconvenient.

The boundary between the layers: facts up, sentence down

The core never touches the file system. Not because the language has no input/output — it has 22 commissions, directory listing among them — but because the “listed” reply carries names only, without sizes, and a disk analyser is made of sizes. They can be obtained only by spawning a process, and that was measured: 8.82 ms per spawn, that is 16.5 minutes over a tree of 111,986 entries against 3.39 s of a native walk. The argument is written at the top of core/disk-inventory.flang and repeated in core/README.md.

So the host gathers the facts and hands them over by value, and the core returns its decision by value too:

The labels on the diagrams are identifiers from the code. Inside the core they are translated into no language at all: МожноУбрать and Кэш are identifiers proved in core/, and the host translates only the word the screen calls them by.

The boundary is drawn along a commission that does not exist, not along a function that is missing. Hence a consequence visible in the tree: the host/internal/clean package never asks the core anything itself — it receives a sentence already passed, together with the finding, and from there it only carries it out.

The road from pressing Backspace to a file that is gone

On the live walk screen Backspace erases for good: there is no trash behind it, and restore afterwards has nothing to work with. This is exactly the place where the tool could have grown a second road to deletion — “the user did point at it, after all”. It did not:

The way to read this: the key decides only which ground the question is asked about. What on that ground may go is none of its business and never becomes its business. A path the layer did not mark cannot be erased by pointing at it harder.

Three places on the diagram hold up the rest:

• the tree is walked again, rather than taken from what the screen was showing: what gets erased is what the core sentenced now, not what was true at the previous measurement;
• the journal goes down in full before the first deletion. After a crash halfway through a move to trash, the files themselves are still there; after a crash halfway through an erasure only the list is left, and the person whose files those were has nothing else to answer “what went” with;
• the file’s fingerprint is checked again between the walk and the erasure. A file that changed since it was judged is refused, not deleted.

How hard the confirmation has to be is also not the screen’s call: the size threshold arrives in the plan as the field порог_крупного from core.Sizer. A screen with its own gigabyte inside would go on calling 900 MiB small after the rule said otherwise.

Deletion lives in one directory, and flang stands guard over it

The rule of the tree: calls that erase and move files — Remove(, Rename(, Truncate( — are allowed only in host/internal/clean/. There they are surrounded by the core’s sentence, a fingerprint check, the trash and the journal. RemoveAll is banned everywhere without exception, comments included: the guard catches the name itself, because there is no call without one.

This is checked by a run rather than by a promise — and the guard is written in the same flang as the core (tools/licensing.flang, 494 lines):

flang io tools/licensing.flang    # код 0 — чисто

In the tree today:

The protection list is worth a close look. “Do not touch my ~/projects” is not an answer to the question “what is this path”, it is an order from the owner of the machine. So it lives with the host, in host/internal/protect, and it can only subtract. A rule able to ADD a file to the plan is not kept there: that would drive an untruth into the proved layer for the sake of a convenient action.

The screen layout: someone else’s library as a submodule, its output in the tree

The layout — how many cells to paint in a bar, where to cut a line, which rows of a section to show at this scroll position — is computed by the flang-tui library. It is wired in as a submodule, not copied:

git submodule status ui-flang/flang-tui
# 6bb627cc45966bfc24cc2680e1eec2196fb2a43d ui-flang/flang-tui

Copying six .flang files would have been simpler. But then the question “where did this line come from and how do I emit it again” would have been answerable only by whoever copied, whereas a submodule answers it with a command.

Here begins the part that made this piece worth writing: the tree holds code emitted by a compiler — 22,596 lines of Go nobody wrote by hand (5,754 in core/out-go, 16,842 in ui-flang/out-go). The argument for why it is there is written down in three places, in the same words: AGENTS.md, core/README.md, ui-flang/README.md. The argument is one — so that a build from a clean clone needs only Go, without the flang compiler. The price is named in three places too: editing anything inside out-go/ by hand is a defect, not an edit, because make -C core печать begins with rm -rf and will wipe it silently.

The flang layout sits behind the flangui build tag and is not the default: without the tag the screen uses the handwritten Go in layout_stock.go (258 lines). The pair layout_stock.go / layout_flang.go (81 lines) has the same names, the same signatures, the same call sites. Changing the layout means changing both.

The two implementations are compared by a run, not by a promise

One build holds one implementation, so they cannot be compared from inside go test: two runs of the same tree with different tags are needed. That is what tools/sverka-ui.sh is for:

tools/sverka-ui.sh
# == снимки кадров: 4 глубины цвета × ширины 40/80/120/200 × 2 языка × все разделы
#    СОВПАЛО байт в байт
# ...
# сверка раскладки: расхождений 0

There is deliberately no reference file of frames in the tree — it would go stale on the first new section, and people would be fixing it blind. What is compared is two runs of one tree: whatever the screen draws, both builds have to draw it the same.

A Mac without cgo: nine symbols and nine jumps

Go has no machine metrics for macOS out of the box, and cgo drags in a C compiler and breaks the static build. host/internal/libsystem takes nine Mach symbols straight out of libSystem.B.dylib — without a single line of C:

//go:cgo_import_dynamic libc_sysctl sysctl "/usr/lib/libSystem.B.dylib"
//go:cgo_import_dynamic libc_host_statistics64 host_statistics64 "/usr/lib/libSystem.B.dylib"
//go:cgo_import_dynamic libc_proc_pidinfo proc_pidinfo "/usr/lib/libSystem.B.dylib"

There are nine such lines in all, and not one import "C" anywhere in the tree:

Each symbol comes with a stub in assembly — one jump, and the address of that jump as data:

TEXT libc_sysctl_trampoline<>(SB),NOSPLIT,$0-0
	JMP	libc_sysctl(SB)
GLOBL	·libc_sysctl_trampoline_addr(SB), RODATA, $8
DATA	·libc_sysctl_trampoline_addr(SB)/8, $libc_sysctl_trampoline<>(SB)

The jump exists because the Go linker resolves the dynamic import by name at link time and binds it at start-up, while the caller needs an ordinary address to hand to syscall.syscall6. The jump is what turns one into the other.

There are two files — libsystem_darwin_amd64.s and libsystem_darwin_arm64.s — and they match line for line: diff between them prints zero lines. The assembler needs the architecture in the file name, not in the code.

Not one external dependency

The host is built on the Go standard library alone. host/go.mod has seven require entries, and all seven point inside the tree through replace: one for the core (flangprogram → ../core/out-go) and six for the layout modules. There is no host/go.sum in the tree at all — there is nothing to fill it with.

The same holds for the checks: there is neither Python nor JavaScript in the tree, and none is wanted. The licence guard and the emitted-code comparison are written in flang, and the compiler needs only cc.

One list of commands and one dictionary

Two things in this tree are kept as data rather than as code, and both for one reason: a list named in three places is three chances to disagree.

There are eight subcommands, and exactly one list of them — cli.Commands (host/internal/cli/cli.go:66). The --help text is taken from it, the COMMANDS section of the live screen is drawn from it, and the manual page digitdisk.1 is checked against it. A disagreement between any two of the three fails go test -count=1 ./..., and in both directions: a flag registered in the code and not named on the page is as much a defect as the reverse.

The screen does not merely show that list, it runs it, and “what happens if you press Enter on this line” lives right there, in the field Start: run it here, close the screen and execute, ask for a path and execute, or not from here — and then the field Instead says where the command does live. The reasoning is stated plainly in the source: this is a property of the subcommand, not of the drawing. Keep it in the screen, and in a month the screen’s list will disagree with the help’s list by one line nobody notices. Safety is separate: purge is not started from any screen at all.

The dictionary is one too, and an entry’s key is the Russian string itself, not an invented name: l.T("СИСТЕМА"). Russian then cannot disagree with itself, and English lies beside it. Today that is 852 pairs across eight files (grep -hoE '^\s+"[^"]+":\s+"' host/internal/lang/dict_*.go | wc -l → 852).

Three boundaries of the translation are drawn hard, and all three are visible in the code:

• every string a person sees has a pair — not a promise but a run: go test ./internal/lang/ reads the host’s source, finds every call to T/F/Say/Errorf and fails on a string without a pair, on Cyrillic in the output packages bypassing the dictionary, on a dead dictionary entry and on % placeholders that drifted apart;
• --json is not translated — the keys and the machine values are the same byte for byte. The Russian words that already travel in JSON as values (the class Кэш, the sentence МожноУбрать) are names of the deciding layer and entries of the journal, not output text. For them there is lang.Phrase: Russian into the file, the reader’s language onto the screen;
• names inside the core are not translated at all. Not one letter in core/ changes with the output language; the host translates only the word the screen calls them by.

What we did not measure

This piece is a walk through the build, not a measurement. It is worth naming the border of the knowledge outright, so that nobody reads more into it than is there.

• Speed we did not measure here even once. The only figure about time in this text — 8.82 ms per process spawn and 3.39 s for a walk over a tree of 111,986 entries — is taken from the top of core/disk-inventory.flang, where the purity of the core is argued, and it concerns a comparison of two roads, not the speed of the tool.
• The cost of the flang layout against the handwritten Go is not named. The comparison has a --замер flag that prints the cost of a frame and of a keystroke in both builds. We did not run it, we have no number, and a guess cannot go here.
• The correctness of the core is not proved in full. 14 postconditions and 185 examples (cat core/*.flang | grep -cE '^ *пример' → 185) are what flang check and flang test verify. Claims such as “the tool will not delete anything you need” do not follow from them: the postcondition “only rubbish may be cleared” is true exactly as far as the definition of rubbish is. The tree says so itself: while the marks were searched for as a substring of the path, the postcondition held, and the tool was wrong four times on a live machine.
• We did not run the two-implementation comparison in this work. The tree was opened read-only; “0 divergences” is what the script prints by its own construction, not our run. The same goes for make -C core сверка (240 inputs): that number is named in core/README.md, not by us.
• Nothing is said about Windows. The tree has libsystem for macOS and procfs for Linux; there is no third branch, and whether one was needed is a question this piece did not go into.
• We compared digitdisk with no other cleaner on quality of analysis. The tree forbids borrowing code from copyleft projects; watching how others work it does not forbid — but a measurement of “who is more accurate” does not exist here.

One line at the end

The version of the tree everything was counted on is 0.8.0 (cat VERSION). The numbers were taken on 3 September 2026 from a working copy; in another commit they will be different, and that is exactly why a command stands beside each one rather than a result alone.