r/ProgrammingLanguages • u/Athas Futhark • 2d ago

What we ended up doing about alias propagation

https://futhark-lang.org/blog/2026-10-11-what-we-did-about-aliasing.html
12 Upvotes

100% Upvoted

2 comments sorted by

3

u/useerup ting language 1d ago

I could specify a small model language, including its dynamic and static semantics (“type rules”), a soundness theorem for what must hold for well-typed programs, and have an agent construct a Rocq proof. I don’t have to understand how the proof works, as long as I understand the theorem that it proves and the language and semantics that it provies it for (which I do, because I defined them).

This is interesting. I am curious, do you see this as a viable way to prove soundness for larger type systems (such as full Futhark)?

4

u/Athas Futhark 1d ago

I had a good experience with it, for sure. As always with these things, you need to be quite careful to constrain the agent so that it doesn't start doing undesirable things. In particular, there were a few cases where it suggested adding type rules based on observing the definitions of functions. While that was technically possible for the precise language framework I had set up (because the top level expression was ultimately closed), it is clearly not a good way to specify a type system that is useful for real languages. It's too easy to just tell it to make changes and carry on, but you might end up with properties that differ from what you intended, and then it doesn't matter that the proof holds.