New versions will ship with [@lemma] march-lang.org/docs/lemmas/ which marks a plain March function that proves something at compile time via Z3 and is erased. A lemma under `cap verified` combines theorem proving with capabilities sot hat the compiler reject code that can't be proven.

March can now infer refinement types for you. march --refine-infer tries candidate contracts, keeps only the ones the SMT-backed checker proves and that close an open obligation without breaking a caller, writes them, then re-checks. Two unproven obligations → two contracts → verified.

In the next version all TLS connections will offer ML-KEM first, and I'm moving towards using that for everything done to secure orchestrated deploys.

I'm rolling out stdlib examples that can run in a repl in the browser. Full coverage may take a few weeks, but some examples work today, and it's a full repl, most valid code should work barring browser limitations like networking or filesystem access. march-lang.org/docs/stdlib/...

March 0.5.0, new since 0.4: • Choreographies: one global protocol, projected to typed per-role endpoints, run across a cluster • Set measures (elts, card) and abstract refinements, via SMT • Epoch-versioned hot reload • Live nodes: remote REPL, actor tracing, forge top, and which code is running

Coming soon: What did the compiler do to my function? `forge query fn handle` lists every pass that changed it and prints the IR after the last. `why-miss` names the input that busted your cache. Add `--json` and an agent can ask the compiler instead of grepping a 10k-line dump.

I'm shipping remote observability and shell tools in the next version. You'll be able to attach to a running node or cluster and diagnose issues, inspect actors, run commands, and so on.

I'm working on a implementation of Choreographic Programming in March, which felt like a natural fit for actor based concurrency, hot reloads, and capabilities. www.fabriziomontesi.com/bliki/Choreo...

Choreographic Programming

fabriziomontesi.com

forgepm.org is getting docs pages for deps!

March 0.4.0 is out: • TRMC is on by default — natural `map` no longer blows the stack • Scheduler threads track your CPU count • Interpreter ~11x faster • Parallel allocation no longer scales negatively • Actor.stop drains instead of dropping github.com/march-language/march/releases/tag/v0.4.0

Release March v0.4.0 · march-language/march

Added Compiled to_string/println render a user ADT's constructor, not #<tag:N>. A boxed constructor cell carries a per-type tag and nothing else, so the compiled backend's type-erased formatter h...

github.com

March 0.3.0 is out. • Capabilities: a hard ceiling, on by default • Actors: timers, bounded mailboxes, supervisor backoff • 128-bit SIMD + narrow NativeArrays • let*, parser combinators, context-aware ~H escaping • Refinement types: structural induction march-lang.org/docs/upgradi...

Check out forgepm.org/packages/dep... ForgePm now scans package tarballs for module capabilities and matches them against a declared manifest. Packages must match their manifest and capabilities are viewable on the package page.

After reading Compile-time Security Analysis and Optimization of Sensitive String Producers arxiv.org/html/2605.16... I've updated Sigils march-lang.org/docs/sigils/ to use contextual escaping.

The next version will include capability audits from the build tools, and file scoped read/write capabilities. You'll be able to see if dependencies use capabilities and compile them out of modules you don't call. A malicious dependency without a file read and network CAP can't exfiltrate files.

Working on an improved refinement type system for version 0.3.0 that allows users to opt into strict evaluation of postconditions.

Version 0.2 is out with better module name resolution for handling A.B.C vs D.E.C. Task spawning under parallel builtins like pmap can now handle much larger workloads within the same level of resources. There is also a bug fix to CSV.

Cool to see that @steveklabnik.com 's @rue-lang.dev is using affine and linear types to consume values that move exactly or at most once. Doing this with intermediate values at compile time is really cool.

Working on a Lean type checker to independently spot check the type system, particularly linear reference counts. Eventually this should cover the whole type system, but probably not the whole RC implementation.

Another nice way to try March is with Scroll github.com/march-langua... which is like jupyter or livebook. Many examples from the website can be downloaded as .scrollmd files and run with forge scroll.serve mynotebook.scrollmd

It's early, but if you want to try out some March packages, a few can be found on forgepm.org, which is itself built with March on the Bastion Framework (github.com/march-langua...).

Version 0.1.1 is out github.com/march-langua...

Release March v0.1.1 — first tagged release · march-language/march

Statically-typed ML/Elixir-hybrid functional language compiled with OCaml 5.3.0. Native (LLVM) + JS + WASM backends, tree-walking interpreter, Perceus reference counting with FBIP reuse, distribute...

github.com