Welcome to cppl Discussions!

[MattCCC]

👋 Welcome to C++L Discussions

Welcome to the C++L community.

C++L is an experimental language - a superset of C++ that adds compile-time laws, proofs, contracts, invariants, refinement-style reasoning, and other verification constructs while preserving ordinary C++ as the runtime language.

The central idea is:

$$C++ \subset C++L$$

C++L verification constructs erase to ordinary C++:

$$erase:C++L→C++$$

The goal is not to replace C++, but to make important properties of C++ programs expressible, checkable, and provable at compile time.

What Discussions are for

Use GitHub Discussions to:

• 💡 Propose language ideas and syntax.
• ❓ Ask questions about C++L.
• 🧮 Discuss laws, proofs, contracts, invariants, and verification.
• 🏗️ Discuss compiler, kernel, LSP, and tooling architecture.
• 🧪 Share experiments and real-world use cases.
• 🔍 Challenge assumptions in the specification.
• 📖 Suggest documentation improvements.
• 🛠️ Discuss integration with existing C++ projects and toolchains.
• 🚀 Share projects or experiments using C++L.

If you have an idea that is not yet concrete enough for an Issue, Discussions is usually the right place to start.

Issues vs. Discussions

Use Issues for work that is already reasonably well-defined, such as:

• confirmed bugs;
• specification inconsistencies;
• compiler defects;
• reproducible tooling problems;
• concrete implementation tasks.

Use Discussions for:

• questions;
• language proposals;
• design exploration;
• RFC-style discussions;
• implementation ideas;
• ideas that still need community input.

When proposing a language feature

It helps to include:

1. The problem you are trying to solve.
2. An example in ordinary C++.
3. What you would like to express in C++L.
4. Proposed syntax or semantics, if you have them.
5. Whether the feature affects runtime behavior or should erase completely.
6. Any interaction with existing C++ semantics.

You do not need to have a complete language design before starting a discussion.

A small motivating example is often more useful than a large proposal.

C++L design principles

When discussing changes, keep the core direction of C++L in mind:

• C++ remains the runtime execution language.
• C++L should remain a superset of C++.
• Verification features must have well-defined semantics.
• Proofs must ultimately reduce to evidence accepted by the trusted verification core.
• Runtime behavior must not silently change because verification syntax was added.
• Unsoundness must be explicit and auditable.
• Compatibility with real-world C++ matters.
• Verification features should scale beyond toy examples to production systems code.

C++L is still evolving, so constructive disagreement about syntax, semantics, proof ergonomics, compiler architecture, and implementation strategy is welcome.

Introduce yourself

If you're new here, say hello below.

Tell us:

• what kind of C++ you work on;
• what brought you to C++L;
• what kinds of bugs or invariants you would like the language to help prevent;
• whether you're interested in the language, compiler, verification kernel, LSP/tooling, or all of the above.

You do not need to be a formal-methods expert to participate.

If you have ever looked at a piece of C++ and thought:

This assumption is critical. I wish the compiler could actually prove it.

then you're in the right place.

Welcome to C++L. 🧩