> We seem to have the same desire for a “cleaned up C.”
That's so great! But sad that no enough ideas and argument came up here. :'(
> How metaprogramming would work?
When it comes to "tactics" in Coq and Lean 4 (i.e. DSL to control the typechecker, e.g. declare a new variable), there are almost equivalent features like "elaborator reflection" in Idris 1/2 [1] (e.g. create some AST nodes and let typechecker check if it's okay), and most importantly, in Scala 3 [2], you could use `summonXXX` APIs to generate new definitions to the compiler (e.g. automatically create an instance for the JSON encoding trait, if all fields of a record type is given).
So the idea is like: Expose some typechecker APIs to the user, with which one could create well-typed or ready-to-type AST nodes during compile time.
Yes exactly, I was considering features from Featherweight Rust [3], some subset of it might be partially applied. But yes it should be super careful on bringing new features in in case of compilation speed.
It's also worth to mention that C compiler itself would do some partial "compile-time eval" like constant folding, during optimization. I know some techniques [4] to achieve this during typechecking, not in another isolated pass, and things like incremental compilation and related caching could bring benefits here.
That's so great! But sad that no enough ideas and argument came up here. :'(
> How metaprogramming would work?
When it comes to "tactics" in Coq and Lean 4 (i.e. DSL to control the typechecker, e.g. declare a new variable), there are almost equivalent features like "elaborator reflection" in Idris 1/2 [1] (e.g. create some AST nodes and let typechecker check if it's okay), and most importantly, in Scala 3 [2], you could use `summonXXX` APIs to generate new definitions to the compiler (e.g. automatically create an instance for the JSON encoding trait, if all fields of a record type is given).
So the idea is like: Expose some typechecker APIs to the user, with which one could create well-typed or ready-to-type AST nodes during compile time.
[1]: https://docs.idris-lang.org/en/latest/elaboratorReflection/e...
[2]: https://docs.scala-lang.org/scala3/reference/contextual/deri...
> Lifetime and compilation speed.
Yes exactly, I was considering features from Featherweight Rust [3], some subset of it might be partially applied. But yes it should be super careful on bringing new features in in case of compilation speed.
It's also worth to mention that C compiler itself would do some partial "compile-time eval" like constant folding, during optimization. I know some techniques [4] to achieve this during typechecking, not in another isolated pass, and things like incremental compilation and related caching could bring benefits here.
[3]: https://dl.acm.org/doi/10.1145/3443420
[4]: https://en.wikipedia.org/wiki/Normalisation_by_evaluation
> Every feature must be crucial.
I want to hear more of your ideas on designing such language too, and what's your related context and background for it BTW, for my curiosity?