Changelog: 1.x

Every release of this major version, newest first, as CHANGELOG.md records it.

1.20 - sort_by + ledger reports #

std.vel gains generic sort_by(xs, key) - sort anything by an Int key function. The ledger uses it for a new report command: sorted-by-amount listing with biggest, smallest, and totals. The CI session exercises it.

1.19 - Standard library sprint #

std.vel grows to sixteen functions, all in Velaris: sort (ensures is_sorted(result)), min/max (ensures membership), sum, keep_if, count_where, join, range_list, is_sorted, insert_sorted; apply_to_each and reverse rewritten with typed lets, dropping their nonempty requirements. Library requires are enforced at importer call sites.

1.18 - Float proofs (real IEEE-754) #

Float promises proven in Z3's floating-point theory - bit-for-bit the machine's arithmetic. The prover refutes real-number identities that rounding breaks, with the exact double as counterexample. FP queries get a bigger solver budget; integer proofs stay instant.

1.17 - Failure-aware proofs #

The prover understands fail / check / try: promises on 'or fail' functions are proven for every returning path, fail-guards become facts on those paths, and fallible callees' promises flow through try and check. CI actions bumped past the Node 20 deprecation.

1.16 - Quantified list proofs #

all_of / any_of with a predicate function; in contracts they become Z3 foralls/exists with the predicate's body symbolically inlined. Fixed a latent soundness-of-reporting hole: an untranslatable requires now aborts the proof instead of being silently dropped (dropped premises manufacture false counterexamples).

1.15 - Native Float and Bool #

Typed LLVM codegen (f64, typed allocas/boundaries); division stays interpreted so divide-by-zero is always a clean error; differential-tested against the interpreter.

1.14 - Record proofs #

Symbolic records (one Z3 value per field): field promises proven, record-aware summaries, records printed in counterexamples.

1.13 - The first real app #

examples/ledger.vel expense tracker; chars/file_exists builtins; typed let enabling empty [] and {}; order-flexible signature clauses; scripted-stdin testing so interactive apps run in CI.

1.12 - Continuous integration #

GitHub Actions matrix (Linux/Windows x 3.10/3.12 x full/minimal deps), dependency-aware suite, CHANGELOG, CONTRIBUTING.

1.11 - Language server #

velaris lsp: standard LSP over stdio. Effect/type errors on every keystroke, full pipeline with Z3 proofs on save; per-file diagnostics (bugs in imported files squiggle in those files). Dependency-free VS Code client bundled in editor/vscode.

1.10 - Formatter #

velaris fmt (in-place, --stdout, --check). Comment-preserving, idempotent, proven meaning-safe by re-running the whole suite on formatted code. All repo examples reformatted.

1.9 - REPL #

velaris repl: loose lines run immediately; fn/record/import definitions pass effects, types, and proofs before joining the session. CLI subcommands (run / repl / version). Unknown functions became a friendly E200 everywhere.

1.8 - Real installation #

pip install ".[full]" and a velaris command. Standard-library search path: import "std.vel" works from any folder.

1.7 - Generics + first stdlib #

for any T with call-site inference and clear conflict errors (bindings shown). stdlib/std.vel: first/last/reverse/index_of/ contains_item/apply_to_each - written in Velaris.

1.6 - First-class functions #

fn(Int) -> Int as a type; pass by name; call through parameters. Only pure functions travel as values, so nothing is smuggled.

1.5 - Unignorable failure #

-> Int or fail, fail "reason", mandatory check { ok / fail } handling, try propagation. Ignoring failure is a compile error.

1.4 - Maps #

{"a": 1} typed Map of K to V; get/has/put/keys/length; typed keys and values; clean E610 for missing keys.

1.3 - Float #

Decimal numbers with NO silent Int/Float mixing - conversion is explicit (to_float, round). Proper negation node.

1.2 - Browser playground #

The real compiler running in-browser via Pyodide. Zero install.

1.1 - Escapes + editor #

String escapes (\n \t " \) with friendly E002; VS Code syntax highlighting.

1.0 - Testers' release #

Multi-error reporting (all broken functions in one run, JSON array for agents), to_text, --version, tutorial.