We do now though, with OxCaml! The local stack allocation mode puts in quite a strong constraint on the shape of the allocations that are possible.

On my TODO list next is to hook up the various O(x)Caml memory profiling tools: we have statmemprof which does statistical sampling, and then the runtime events buffer, and (hopefully) stack activity in OxCaml's case from the compiler.

This provides a pretty good automation loop for a performance optimising coding agent: it can choose between heap vs local, or copy vs reference, or fixed layout (for SIMD) vs fragmentation (for multicore NUMA) depending on the tasks at hand.

Some references:

- Statmemprof in OCaml : https://tarides.com/blog/2025-03-06-feature-parity-series-st...

- "The saga of multicore OCaml" by Ron Minsky about how Jane Street viewed performance optimisation from the launch of OCaml 5.0 to where they are today with OxCaml https://www.youtube.com/watch?v=XGGSPpk1IB0

> infer or constrain the amount of copies and allocations a piece of code has

That's exactly what substructural logic/type systems allows you to do. Affine and linear types are one example of substructural type systems, but you can also go further in limiting moves, exchanges/swaps etc. which helps model scenarios where allocation and deallocation must be made explicit.

Allocations and copies are one of the things substructural typing formalizes. It's how E.g. Rust essentially eliminates implicit copies.

There are ongoing projects like Granule[1] that are exploring more precise resource usage to be captured in types, in this case by way of graded modalities. There is of course still a tension in exposing too much of the implementation details via intensional types. But it's definitely an ongoing avenue of research.

[1] http://granule-project.github.io/granule.html

Wouldn't such analysis in the general case run afoul of Rices theorem?

There is discussion about this in the Rust world, though no attempts at implementation (and yet further from stabilisation)