$cat ~/posts/extensoes-bend2-vscode-nvim

bilingual · en / pt

← /blog

i built two bend2 extensions in a week

2026-09-29·en·11 min read·bendlanguagesvscodeneovimtooling

Bend2 shipped, and since I had already written about its idea, the natural next step was to actually use it. But using a new language in the editor I open every day means, in the first minute, a .bend file with no colors, no formatting and nobody telling me I got something wrong. So instead of waiting for someone else to do it, I built two: one for VS Code and one for Neovim.

I had never made a VS Code extension. I had touched Neovim config and small plugins, but never language support from scratch. This post covers what they do, how they were built, and where I stumbled. Spoiler: it was a lot more fun than I expected.

the two extensions

Both are Apache-2.0, public, and cover almost the same list, each in its editor's idiom.

bend2-vscode, published on the Marketplace as Bend 2 Language Support by Nuxyel:

  • syntax highlighting, snippets, language configuration and formatting
  • a language server with hover, signature help, symbols, go-to-definition, references, rename and call hierarchy
  • compiler diagnostics in the Problems panel
  • 21 commands: check, build, run, compare backends (JavaScript, native, GPU), benchmark, project gates and more
  • Proof Explorer, a sidebar with the project's laws and the state of each proof, plus Test Explorer integration
  • it also works in VS Code Web, minus the commands that need to launch bend

bend2-nvim, a pure Lua plugin:

  • filetype, syntax, indentation, snippets and formatter
  • completion, signature help, symbols, navigation, references, rename and diagnostics
  • :Bend2Check, :Bend2Build, :Bend2Run, :Bend2CompareBackends, :Bend2Benchmark and the rest of the family
  • :Bend2Proofs, the Proof Explorer in a buffer
  • Base completion pulled from the compiler itself (bend base), asynchronously
  • no Node, no external LSP server, no dependency on other plugins, no key maps forced on you

In both, whatever doesn't need the compiler keeps working without it installed. Without bend on the PATH you lose check and proofs, but not the editor.

how they were made

In VS Code the architecture is the textbook one: a thin client (extension.ts), a TypeScript language server speaking LSP, and a toolchain package that knows how to find bend, detect its version, run processes and cancel them. Highlighting is a 41-line TextMate grammar, which surprised me: for a language with def, type and law, very little gets you a decent result:

{ "match": "\\b(law)\\s+([A-Za-z_][A-Za-z0-9_]*)",
  "captures": { "1": { "name": "keyword.other.law.bend" },
                "2": { "name": "entity.name.function.law.bend" } } }

The rest of the VS Code side is volume: 21 commands, a view container, the Test Explorer, the release pipeline. The part I didn't expect is that everything also has to run in the browser (VS Code Web has no processes, only a worker), so the parser ships in two wrappers.

In Neovim it was the opposite: no framework, just the editor's own APIs. vim.system to run the compiler, vim.diagnostic to show errors, omnifunc for completion and Lua modules for everything else. There isn't even an LSP server: the intelligence lives inside the plugin itself. The modules: parser, workspace, formatter, toolchain, proof, editor. It adds up to a little over 2 thousand lines of Lua, much less than the VS Code side, because Neovim already ships almost everything the plugin needs.

The workflow was similar on both: first a plan for what a stable v1 needed, then the implementation, with one fixed rule: one small commit per logical delivery. That produced a history you can read like a diary. The Neovim one, for example, starts at feat: add Bend2 filetype and syntax support and moves through the parser, formatter, navigation, diagnostics and proofs, in the order each piece started working.

where it hurt

there is no AST to consume

This is the biggest difficulty of all, and it affects both extensions. A decent language server wants to know where each declaration ends, which names exist, what type each one has. The Bend2 compiler exposes none of that in a stable way. It does check, run, build and prints errors. Whatever "semantics" the extension knows comes from a hand-written tolerant parser that reads line by line, strips comments and strings, and recognizes def, law, type and import:

local keyword, name = declaration:match("^(%a+)%s+([A-Za-z_][A-Za-z0-9_.]*)")
if keyword == "def" or keyword == "law" or keyword == "type" then
  -- becomes a symbol, with range and selectionRange
end

It works well for navigation and so-so for the rest, and the rest is the problem: hover, signature help and the inferred "proven" state are approximations. The decision I made (and it's written into the repository's principles) is to never sell an approximation as truth: whatever comes from the parser is marked provisional, and only the compiler can say a law was verified. The VS Code 2.0 roadmap is literally "when the compiler exposes types, spans and proof context, throw my parser away".

reading the compiler's error as text

Without structured diagnostics at the start, the extension read the human output. A Bend error looks like this:

Error:
- expected : a name (got the keyword 'match')
- observed : ' '
Location:
1 | def unfinished(value: Nat
2>|   match value

You can parse Error: and Location:, but you're coupled to the text of one specific version. I still keep a fixture captured on Bend 2.0.23 as "legacy". Today the plugin asks for --diagnostics=json when the compiler supports it and falls back to the text parser if not:

local args = { path, "--check-only" }
if config().diagnostics_mode ~= "text" then args[#args + 1] = "--diagnostics=json" end

Note the --check-only. That flag exists for a very concrete reason: checking a file must not execute its main. In a language whose main can print, read an environment variable or do IO, "check on save" that runs the program would be a security bug and a terrible surprise.

the language moves faster than you

Bend2 is new, so the compiler version is part of the contract. The rule became: minimum 2.0.28, anything below shows up as unsupported, and CI runs the matrix against 2.0.28 and 2.0.32, each downloaded at a pinned version with the official checksum verified. The repository's own proof project is compiled by both on every push. If bend changes the format of an error, the test breaks before a user notices.

a rename that renames too much

Cross-file rename looks easy until two modules have a function with the same name. Rename and references by name could edit the homonymous declaration in another file. The fix, two commits (fix: resolve cross-file references before rename and test: prevent rename across homonymous imports), was to confirm each candidate by resolving its definition through the import before editing. In Neovim the same risk was handled by the commit fix: resolve Bend workspace symbols by declaration identity. Rename by text is a trap, even with a dumb parser behind it: the declaration has an identity, and the word doesn't.

the Neovim gotchas

Almost every "Neovim" difficulty was an API detail nobody warns you about:

  • vim.system callbacks run in a fast context, where you can't touch buffers. The Proof Explorer smoke test broke because of it, and the fix was to wrap everything in vim.schedule_wrap.
  • foldmethod is a window option, not a buffer option. The autocmd assigned it as if it were buffer-local, and the automated tests caught the defect.
  • An async check result arrives late. If you edited the buffer while the compiler ran, publishing the stale diagnostic paints an error on the wrong line. Each result is now discarded if the buffer's changedtick changed since the check started.
  • nvim -u NONE doesn't turn on filetype detection. I found this taking the README screenshots: the buffer showed no highlighting and I was sure the extension was broken.
  • macOS is not Linux. The unit suite passed locally and failed on both macOS CI jobs, and the fix was the commit test: compare canonical workspace paths on macOS. Without the macOS runner I wouldn't have found it.

porting the official formatter

Bend2's real formatter is bend-fmt-lsp, from the official repository. It makes no sense to invent another, so both extensions carry an adaptation of its lexer and rules: in TypeScript on VS Code, in Lua on Neovim, both with an attribution header in the file and, on Neovim, a NOTICE with the same license. That was also a project decision: when an official truth exists, the extension's job is to follow it, not to have opinions. The Lua version did drift out of sync with the official contract, and the release review caught it before the tag.

the last mile is bigger than the code

I thought "the extension is ready" and "the extension is published" were almost the same thing. They aren't. A few publishing stumbles, all real:

  • the release workflow broke on the GitHub runner because a quoted shell expression that worked locally wasn't interpreted there
  • the provenance generator still wrote 0.1.0 into the file of a 1.0.0 VSIX; the post-commit validation caught it, and the fix came with a permanent check tying the metadata to the manifest version
  • the Marketplace rejected the name: "Bend 2 for VS Code" already existed. I cut a 1.0.1 just to change the displayName to Bend 2 Language Support by Nuxyel, and left 1.0.0 untouched with its SBOM
  • creating a publisher, an Azure DevOps token with Marketplace (Manage) scope and a GitHub secret is a mini-tutorial of its own
  • after everything was uploaded, it still sat in verifying for a while

On the Neovim side the last mile was lighter, because there is no store: a plugin is a Git repository with SemVer tags. I documented lazy.nvim, vim.pack (Neovim 0.12+) and the native package layout for 0.11, and added a pkg.json as metadata only. There is no LuaRocks package and no registry.

using bend2 inside the extension

A question I asked myself midway was "where do these extensions use Bend2 itself?". Besides calling the compiler for everything, both have a real Bend project inside the repository, used as an example and as the dogfood test: a model, a laws file and a proofs file.

law adding_zero_preserves_value:
  for value: Nat
  {Model.add_zero(value) == value : Nat}

def add_zero_right(value: Nat) -> {Model.add_zero(value) == value : Nat}:
  match value:
    case 0n:
      {==}
    case 1n+predecessor:
      %add_zero_right(predecessor) : {1n+Model.add_zero(predecessor) == 1n+_ : Nat}
      {==}

CI checks that Bend accepts that proof, and the Proof Explorer shows the law as verified by the compiler. Two nice things here: the example and the test are the same file (one copy to keep), and seeing a proof language run in the editor built for it feels good in a way I can't quite explain. In the Neovim one, Base completion also comes from the compiler, which knows how to list what exists.

why this is fun

I went in expecting editor bureaucracy and found the opposite.

The feedback is immediate and visual: you tweak a grammar rule and the color changes, you write a hover and it shows up. Few projects respond that fast.

You also get to see the language from the inside. To build an extension you have to understand every Bend2 construct, what +d is, what 1n+p is, how a law connects to its proof. I learned more about the syntax writing the parser than reading the documentation.

The missing AST helped, in a strange way. It forced me to decide what is fact and what is guess, and to write that into the interface. I'd take that product honesty to any project.

And CI turns the whole thing into a kind of level-based game. The Neovim plugin only got its v1.0.0 tag with 12 green jobs: Neovim 0.11.7 and 0.12.5, Bend 2.0.28 and 2.0.32, Linux and macOS. Each combination that passes is an unlocked level, and the macOS level showed me a bug I would never have found on my own.

If you use Bend, install one of the two and open an issue when something breaks; if you've never built an editor extension, this is my invitation: pick a small language and build one. You'll most likely get lost halfway and love it.