The @unsafe count is disclosed only on the no-main path: a harmless main, or any -o emit/build, reports nothing

What you did

One fixture, three commands. main.bend imports PROOF.bend, which imports unsafe.bend (@unsafe def contradiction() -> {0n == 1n : Nat}):

• bend PROOF.bend (no main)
• bend main.bend (main = 7)
• bend main.bend -o main.js and bend main.bend -o main (emit / build)

What happened

bend PROOF.bend:

1 term annotated as unsafe.
The code is well-typed, but may contain logical paradoxes.

bend main.bend:

7

-o main.js and -o main: no output at all. Exit 0 in every case.

The only @unsafe disclosure comes from the no-main path; a harmless main (or any -o) drops it while the unsafe def stays in the import graph. In bend2/main.ts at 0b7e2b11, cli_report (line 397) is the only place the count is printed, book_run calls it only in its no-main branch (lines 454-460), and cli_emit (line 196) never reports it. Reproduced on 2.0.4 and 2.0.5. (Related: #776 covers the proof-mode exit code; this one is the disclosure vanishing in run/emit.)

The file

import Base
import ./PROOF.bend as P

def main() -> U32:
  7

(the other two files: PROOF.bend states a law discharged by U.contradiction(); unsafe.bend holds the @unsafe def contradiction() -> {0n == 1n : Nat}: contradiction())

bend --version

bend 2.0.5 (2.0.4 the same)

uname -sm

Linux x86_64

clang --version (the first line)

clang version 21.1.7 (Fedora 21.1.7-1.fc43)