Turtles all the way down
See the code
Chelis is a numerical computing language for code that agents write and people supervise. Tensors carry named dimensions and precision in their type, and a proof stack checks the properties you state.
def portfolio_return(w: tensor[3, f64], r: tensor[3, 1, f64]) -> tensor[f64] = {
weighted = mul(w, r)
weighted |> sum(0)
}
In numpy, returns shaped 3 by 1 stretch against three weights into a 3 by 3 grid and
the sum comes back as a plausible wrong number. chelis check rejects the same
multiply before anything runs. The error from its JSON report:
{"kind":"DimensionMismatch","message":"tensor rank mismatch: 1 dims vs 2 dims","severity":0.8,"span":{"span":"point","offset":94},"span_id":"surf:94..103"}
f32 and f64 do not mix without a cast,
I/O appears in a function's effects, and random operations take explicit keys.chelis check answers in JSON with the error kind and
source span, and the same input always gets the same answer. chelis tide mcp
gives an agent check, eval, prove, and structural edits as MCP tools.chelis prove checks @property declarations with
type checking, an SMT solver, or seeded sampling, and each result names the
method behind it. A second checker written in Chelis cross-checks the compiler,
and a core calculus of Chelis is mechanized in Lean 4..ch) is the readable syntax; Deep (.dp) is
the canonical form the compiler and agents use. Programs build to C. Shells,
installed with Reef, cover numerical methods (Nautilus), dataframes (Coral), and
quantitative finance (Shoals).Chelis releases include chelisup, which installs toolchains and selects the
version used by each project. chelisup downloads public releases without a
GitHub token. The commands below sign in with gh to
find and fetch the latest release.
gh auth login
gh release download --repo Chelis-Lang/chelis --pattern chelisup.sh --output - | sh
# If the bootstrap says ~/.chelis/bin is not on PATH:
export PATH="$HOME/.chelis/bin:$PATH"
release_tag="$(gh release view --repo Chelis-Lang/chelis --json tagName --jq .tagName)"
chelisup install "${release_tag#v}"
chelis --version
The bootstrap script installs chelisup; the next command installs the
compiler. The release tag has a leading v, while chelisup install takes
the bare X.Y.Z version. For a project with a reef.toml, install the
version named by its compiler pin before running chelis reef setup, then
run chelis reef build. The install guide
explains the project workflow.
MIT
chelis build app.ch --output out/
./out/app
build invokes the native compiler and links the runtime carried by this compiler.
Definitions-only modules produce static libraries. Sources and headers remain
available; --emit-c keeps source-only builds. CPU is the primary acceptance lane;
HIP and Metal are prerelease targets with known imperfections. See the
backend guide for tool requirements, artifact names,
compiler overrides, and library linking.
Turtles all the way down
See the code
Chelis is a numerical computing language for code that agents write and people supervise. Tensors carry named dimensions and precision in their type, and a proof stack checks the properties you state.
def portfolio_return(w: tensor[3, f64], r: tensor[3, 1, f64]) -> tensor[f64] = {
weighted = mul(w, r)
weighted |> sum(0)
}
In numpy, returns shaped 3 by 1 stretch against three weights into a 3 by 3 grid and
the sum comes back as a plausible wrong number. chelis check rejects the same
multiply before anything runs. The error from its JSON report:
{"kind":"DimensionMismatch","message":"tensor rank mismatch: 1 dims vs 2 dims","severity":0.8,"span":{"span":"point","offset":94},"span_id":"surf:94..103"}
f32 and f64 do not mix without a cast,
I/O appears in a function's effects, and random operations take explicit keys.chelis check answers in JSON with the error kind and
source span, and the same input always gets the same answer. chelis tide mcp
gives an agent check, eval, prove, and structural edits as MCP tools.chelis prove checks @property declarations with
type checking, an SMT solver, or seeded sampling, and each result names the
method behind it. A second checker written in Chelis cross-checks the compiler,
and a core calculus of Chelis is mechanized in Lean 4..ch) is the readable syntax; Deep (.dp) is
the canonical form the compiler and agents use. Programs build to C. Shells,
installed with Reef, cover numerical methods (Nautilus), dataframes (Coral), and
quantitative finance (Shoals).Chelis releases include chelisup, which installs toolchains and selects the
version used by each project. chelisup downloads public releases without a
GitHub token. The commands below sign in with gh to
find and fetch the latest release.
gh auth login
gh release download --repo Chelis-Lang/chelis --pattern chelisup.sh --output - | sh
# If the bootstrap says ~/.chelis/bin is not on PATH:
export PATH="$HOME/.chelis/bin:$PATH"
release_tag="$(gh release view --repo Chelis-Lang/chelis --json tagName --jq .tagName)"
chelisup install "${release_tag#v}"
chelis --version
The bootstrap script installs chelisup; the next command installs the
compiler. The release tag has a leading v, while chelisup install takes
the bare X.Y.Z version. For a project with a reef.toml, install the
version named by its compiler pin before running chelis reef setup, then
run chelis reef build. The install guide
explains the project workflow.
MIT
chelis build app.ch --output out/
./out/app
build invokes the native compiler and links the runtime carried by this compiler.
Definitions-only modules produce static libraries. Sources and headers remain
available; --emit-c keeps source-only builds. CPU is the primary acceptance lane;
HIP and Metal are prerelease targets with known imperfections. See the
backend guide for tool requirements, artifact names,
compiler overrides, and library linking.