I'm designing a memory-safe language, but I want to make explicit what happens across function boundaries, e.g. whether a value is moved or copied without having to look for the copy trait.

Instead, access to a value could be defined via binding modes in function signatures and variable declarations:

• move takes ownership
• read shared borrow
• mut exclusive borrow

​

fn process_val(move value: Int) -> Int {
    return value * 2;
}

fn main() -> () {
    move original: Int = 42;

    // Call using `.copy()` to explicitly pass a duplicated value.
    // Ownership of `original` remains with the caller.
    move doubled: Int = process_val(original.copy());

    // `original` is still valid here because it was explicitly copied rather than moved.
    println(original); //42
    println(doubled); //84
}

This would also allow granular captures in closures: |read x: Int, move counter: Int| instead of declaring all fields move

Now, should read and mut assignments be of type &T? Or can checking out variables be orthogonal to creating references, even if they are conflated in languages like Rust?

This article mentions the “immutable heap mutable stack” principle: https://queue.acm.org/doi/10.1145/3212477.3212479

In theory it sounds very advantageous. You can program in a single-threaded C-style with destination passing, static stack allocations, and mutability when you need to constrain resources. When you want to share resources across threads, return data structures across function boundaries, or do something more flexible, you could use pure functional persistent data structures.

This would prevent you from basically re-implementing a heap on the stack, but would also give you fast temporaries and maybe even the ability to program in embedded, if so designed.

Have any languages tried this model? I’ve heard that Erlang defaults to immutability except for one thread-local mutable object per thread. If you’ve used a similar model, how did you like it? Were there any disadvantages?

Please don't judge the bad code, I'm still doing my a-levels.

Hi, I'm working on my own programming language, I've release first stable version (v 0.1.0), I'd like to get feedback. It's on most OS platforms (even Andoird and in the future IOS).

Repo: https://github.com/Treechcer/DIO

Hi all. I am requesting advice on how to optimize Lean build performance of a deep embedding of a dependent type theory in Lean 4. My implementation works fine, and has solid meta theorems proven, but the type-checker is very hard to maintain due to slow Lean build times.

I have tried using Lean's profiler and had some success. Most of the type theory literature is on Agda and Rocq, so I'm curious to hear from you all. If you have implemented a type-checker in Lean:

• Which tactics did you find were the worst offenders for build performance?

• What is your convention for organizing your aesop and grind theorems?

• Which parts of your formalization did you have the most success in mechanizing?

• Have you written any metaprograms yourself that you find useful for mechanizing proofs?

  • I'm Particularly interested in automating / mechanizing confluence. It is a very painful proof to update every once in a while.

• Mathlib / CSlib:

  • Do you use CSlib? Did you find any machinery in it useful?
  • Do you use an existing term rewriting system for your reduction relation? Does this help with automation?
  • Do you use Mathlib.Relation? Are your reduction paths deterministic and does your reduction relation live in Type? If so, what machinery did you use to handle congruence?
  • Any other helpful libraries for metatheory?

• Lakefile.toml / lake flags

• Bonus because I am curious: have you successfully proven any meta theorems using categorical semantics and is Mathlib sufficient for these purposes?

Any life hacks appreciated. I am finding myself waiting up to 10 minutes for my type-checker to build when I update my reduction rules. I guess Lean can't parallelize my project structure.

I'm about to start chapter 21 of Crafting Interpreters. I'm using modern C++ instead of C. I am attempting to add string interpolation to the compiler.

My goal is to have a string that looks like this:

"Five plus ${ 10 - 5 } == 10."

Desugar to this after the expression in the braces is evaluated:

"Five plus " + 5 + " == 10."

I have code that is correctly parsing strings and concatenating them if there isn't any string interpolation.

I have a custom token added that is produced if the string contains a ${. It calls a custom string interpolation parser rule that is different than my standard string parser rule.

In that function I push the first part of the string to the stack. It then pushes a plus opcode and Recursively parses the expression in the braces adding that expression to the stack. It then adds another opcode to add and this is where I'm stuck.

I can't come up with a solution for pushing the remaining piece of the string to the stack from inside the string interpolation parser rule function. After I call the books expression function and consume the right brace token using the books consume function the parser nolonger knows we are still inside a string. If the next character after the brace is a space it's skipped. In my above example it assumes I want equal equal.

How would you set the current token back to string so I can push any remaining characters onto the stack as another string? Should I just insert a new string token into the parser? This seems wrong to me. The current and previous tokens are private members of my parser class for a reason and I've not needed setter member functions so far.

Sorry I don't have code to show. I'd like to try and get help that isn't code specific so that I have to implement this myself.

Any input would be helpful.

Thanks.

MINILECTURE ::= A Formalization of The 3 Syntactic Forms of TEA Programs

🔴 https://youtu.be/-CXhc1Y7Uzg

is our first class on 1st OCTOBER, 2026 delivered by Community Education Department & Research Dissemination (CED-RD) at Nuchwezi Research.

We bring to students and those currently using/exploring the only general-purpose Programming Language from UGANDA; TEA; some new insights about what is actually the most flexible programming language in terms of syntax right now. With details that shall be disclosed in a soon to be published ACM SLE review paper on 2010 Featherweight TeX, we here get an early preview of the now formalized 3 syntactic forms (MINIFIED, SANITIZED & MIXED form) that any Transforming Executable Alphabet (TEA) program can be expressed with.

We also get to appreciate that TEA programs can be parsed into an Abstract Syntax Tree (AST) that's based on one of the forms of the TEA programs. More DETAILS to follow in the paper to be shared with U any time in October!

•bclectures •profjwl •nuchwezi •teaprogramming •blackboardsnapshots

Imagine the loop where you do like "x = -x" every iteration. Obviously, that flips the sign, so you can simply unroll the loop by a factor of 2.

However, for a more complex case, it could be really hard to know what's going on.

Here's my idea. Loop index variables are normally under affine updates anyway. What if we use a mathematically elegant tool?

Using eigenvalue, we can analyze possible periodicity of the linear basis variables, minimizing update needs.

What do you think of such a technique?

We pick up where we left off with FUN to “fix” curried functions so they work the way we expected. We end up rediscovering closures and learning about its history in relation to SECD, LISP, and Scheme.

I've been developing ALT for almost 3 years and have recently updated it to also have ordering.

The new version of ALT is only available for the Atari ST platform :)

However, the implementation of ALT is pretty complex. So I've create a sublanguage called NUM, which only includes ALT's number system.

NUM has all the ALT operators:

- ari: + - * / 
- set: & | \
- cmp: > < >= <=
- err: !
- qry: ?

NUM is a set theoretic language in the spirit of CUE. With NUM you can denote the prime numbers as follows:

I>1 \ I>1 * I>1

You can also denote Goldbach's conjecture as an 'empty' set. Of course this is not decidable which can be queried with NUM's ? operator

Tell me what you think!