Facet

A hybrid C++/Webview IDE for Lean 4. Combining the speed of a systems editor with the rich interactivity of a proof assistant.

Core Architecture

To achieve "faster than VS Code" while integrating Discord-like features, we use a hybrid native/webview architecture.

1. The Engine (Rust/C++)

The core text buffer and language client are native. This ensures near-instant startup and zero-latency typing (like Zed). It communicates directly with the Lean 4 language server.

2. The Modular Browser (Webview)

Lean 4 requires a rich HTML "InfoView" for proof states. We use Tauri/Webview to render these panels as detachable tabs.

Social Coding

Facet integrates Contextual Collaboration directly into the editor.

• CRDTs: Conflict-free editing for real-time pair proving.
• Proof Rooms: Voice channels attached to specific files or theorems.
• Anchors: Chat threads anchored to logical states, not just lines of code.