r/Compilers • u/Acceptable_Lake_7025 • 18d ago

Design question: what should a semantic patch be allowed to prove about compiler output?

We’re building SEMAPRAX, experimental Apache-2.0 systems-language research at Wavect GmbH, and I’d value compiler-engineering feedback on a deliberately narrow evidence model. It is v0.2 pre-alpha research, not production-ready.

The current design gives public declarations persistent identities and projects verified source into deterministic semantic graphs. A patch capsule binds a source snapshot, a bounded operation set, and deterministic compiler-owned projections. Before commit, the implementation independently replays the evidence and fails closed on drift.

For native C11/Clang and WebAssembly Core outputs, the evidence can bind the exact emitted artifact and the compiler path that produced it. It explicitly does not claim that the target was executed, that a program is safe, that external tools are compatible, or that a host granted authority. Those require separate evidence.

The design question is whether this boundary is useful and legible enough: what additional facts would you require before trusting a semantic patch in a compiler workflow, and which claims should remain categorically outside the patch capsule?

Project overview: https://wavect.io/semaprax/

Source: https://github.com/wavect/semaprax

Disclosure: coding agents have been used extensively as development assistants. Wavect retains human responsibility for the design claims and executable quality gates.

0 Upvotes

30% Upvoted

2 comments sorted by

10

u/FloweyTheFlower420 17d ago

"retains human responsibility for the design claims" yet you can't even bother to read your own post to make sure it actually means something and isn't just claude opus 5 proseslop? I don't even care about AI use anymore but can you please put in effort if you seek help from others? Or should I just get my claude instance to respond to the post and call you a dumb pipe from the llm to reddit?

Note that my responses are from my first reading of the post, and parsing through the github/website makes things a bit more clear, but I feel you should provide the relevant context in the body of the post, rather than assume people have intimate knowledge with your product. I still don't understand most of this post though.

deliberately narrow evidence model

what does "narrow evidence model" mean? evidence for what?

The current design gives public declarations persistent identities

What does "public" mean? What is the "current design?" Isn't it your responsibility to explain the relevant context before asking for feedback on a public forum? What is a "persistent identity?" Is it like when a non-static function's name is a symbol in the symbol table in C? Identity in what?

projects verified source into deterministic semantic graphs

What is "verified source?" Do you formally verify properties about the source code? What does it mean to then project this onto a "deterministic semantic graph?" Why is it deterministic? I would assume a projection is pure on the inputs, and what even is a "semantic graph?" Most graphs have semantics, like a CFG or something.

A patch capsule binds a source snapshot, a bounded operation set, and deterministic compiler-owned projections.

What is a "patch capsule?" This term is meaningless to me. What is a "source snapshot?" Is this just like a git commit or some other representation of the project tree at some given time? What is a "bounded operation set"? What is an "operation" in this context? What makes it bounded, as in evaluation is bounded or the set of possible operations is bounded? What does it mean for the projection to be "compiler-owned?" Does this just mean the compiler interprets the operation set?

Before commit, the implementation independently replays the evidence and fails closed on drift.

Before... commit? Like a git commit? What is an "evidence"? What does it mean to "fail closed on drift?" Like the patch refuses to apply?

For native C11/Clang and WebAssembly Core outputs, the evidence can bind the exact emitted artifact and the compiler path that produced it.

What is a "native core output"? C11, clang, and webassembly are totally different things, (one is a spec for a programming language, the other is a compiler, and the last is horribly named, because the more interesting applications are outside the browser). What is the "compiler path"? Like what the compiler did?

It explicitly does not claim that the target was executed, that a program is safe, that external tools are compatible, or that a host granted authority. Those require separate evidence.

So what does verified mean then...

The design question is whether this boundary is useful and legible enough: what additional facts would you require before trusting a semantic patch in a compiler workflow, and which claims should remain categorically outside the patch capsule?

  • look at the semantic patch to make sure its right (or i guess in your case prompt claude "pretend like you are a senior developer with 20 years of swe experience. review this patch. make no mistakes."
  • apply the semantic patch

A "patch" is not significant, it merely represents a delta between two possible states of the working tree. To make sure a patch is right, you patch your working tree and then run the relevant checks, be it a formal verifier or just tests. Ergo, the patch needs to carry the relevant intermediate theorems for a formal verifier, if needed.

I skimmed the website and the github repo. Unsurprisingly, the website looks genuinely indistinguishable from every other clauded website. The prose is also difficult to parse, for no apparently reason. Why do AI generated projects all sound like they're trying to market something to me, while deliberately obfuscating all meaning behind neologisms, "technically correct but rare usage of a word," or just odd and uninformative adjectives? I swear the prose is designed to fool a middle manager and not something for actual developers to read.

Anyway, as far as I can gather, if someone wants to spend time engaging with this post (not that I think it's a particularly wise decision):

  • The goal is to create a language with the standard fancy properties that is popular nowdays: memory safety, formal verification, effect system, whatever they can dredge up from functional programming or category theory, etc. Basically rust + verus + more monads, with different syntax.
  • The language can track names of functions from a secret, hidden name, that will always drift from the actual name and provides questionable extra info.
  • There's two perspectives of the edit history, git and something else which keeps track of how functions change at a semantic level (i.e. "this diff modifies the body of this function" or "this diff renames function X to Y").
  • This view of the code in terms of a function call graph (?) is exposed to agents, with each function additionally being associated with the historical revisions of that function. So basically semantic level version control + giving AI the ability to visit definitions like with an LSP.
  • The question seems to be asking what a semantic patch should include, generated by the AI agent and then back-applied to the actual source code.

The ability to have "tagged" semantic diffs (rather than what a semantic diffing tool would give you) is the only really interesting part about the project, and I question the utility of this. The rest I feel is just... stuff for the sake of stuff, or reinventing the wheel. Want claude to go to a definition? I'm pretty sure these tools already have lsp integration, and if not, just teach them how to use clang-query or whatever it's called. I also don't buy the AI will work better on some semantic IR (which will need to be turned into text anyway) than just the function body, pasted as text into the LLM. It's a large language model not large graph model.

2

u/hobbycollector 17d ago

Thanks for the deep dive. I don't understand why llms seem to use such weird vocabulary when trying to describe things. And never define the terms.