Rust/Pony like ownership for Go: Gown for data-race freedom at compile time

[Jason E. Aten]

https://github.com/glycerine/gown

With Gown, channel sends can now enforce at compile 

time Go's "convention" of transfer of ownership. 

Gown is a pre-processor for Go, turning .gown files into .go

files. It can be layered on top of existing code, and adopted

incrementally. The readme is a tutorial. 

I had LLM help but the formal proof of design soundness 

was mechanically checked by the LEAN theorem prover. 

The test suite is robust, but I may not have thought of everything.

== Call for testing and user experience feedback ==

Please try gown and file issues with bugs and feedback.

There may still be implementation bugs that do not catch all data races.

Call for testing: Help us polish and refine Gown by 

trying it out! File bug report issues to help us improve!

Thank you, and enjoy!

Jason

[Robert Solomon]

My question is, how do you create your .gown files?   A Go IDE would choke over your \iso, ... stuff

Let's say I use vim, then I would lose the power of an IDE, like VS code or Goland.

How do you handle the problem of losing the power of an IDE?

Rob Solomon

[Jason E. Aten]

Hi Rob,

That's kind of the tail wagging the dog, right?  But I agree it is awkward. I don't really want to rename 

the .go files to .gown in my large code bases. The solutions look to be either

a) teach IDEs to understand the .gown syntax; or

b) offer a comment based syntax in .go files that does the same thing as a .gown file

For now (b) seems the easier, more incremental path. I dislike how it looks and how clunky it feels, but I did it anyway.

That is, I've done an initial attempt at it here, on the "comment" branch.

https://github.com/glycerine/gown/tree/comment

Try that and let me know how you get on. The status part of the README has examples

of the comment style annotation, as do the vectors/ examples. 

Jason

[Robert Solomon]

I don't understand why the comment below says "result 0 imm".  Why the 0 in that line?

And, I don't understand why you declare fmt.Printf to be an observer.  What should be declared an observer and why?

//gown: param goner iso; param spare rob; result 0 imm

func puncture(goner *wheel, spare *wheel) *report {}

//gown:observer fmt.Printf
//gown:iso
//gown:clone
//gown:new
//gown:swap

comment branch to attempt to imporove usabilty

That's a typo that should be improve.  

[Jason E. Aten]

Hi Rob,

Reasonable questions. 

(Pull the latest comment branch where I have tried to answer them and allow named return annotation.) 

Also inline here, with more detail:

Q1. Re "why 0 on that line"?

The "result 0 imm" is saying that the first (0-th) return value should have an \imm ownerstamp.

As a Go func can have dozens or more return values, and they can be all named or all un-named,

this syntax is a regular and uniform way to indicate which of the return arguments the

ownerstamp annotation should apply to. 

In this case it is the first return value. We are simply numbering the unnamed arguments, starting from 0. 

I'm open to suggestions if you have a more intuitive syntax, but this is the best I have come up. This is

the klunky part I mentioned before.

If we had in .gown a 

func f() (answer \iso *int) { ...

then we could have .go comment format as:

//gown: result answer iso

func f() (answer *int) { ...

here are some more examples from vector/ex4/main.go which I added to illustrate:

// gown: result answer iso                                                              
func f() (answer *bicycle) {
    return &bicycle{} //gown:new                                                        
}

// gown: result answer iso                                                              
func ff() (anum int, answer *bicycle) {
    return 7, &bicycle{} //gown:new                                                      
}

// gown: result 0 iso                                                                    
func g() *bicycle {
    return &bicycle{} //gown:new                                                        
}

// gown: result 1 iso                                                                    
func h() (int, *bicycle) {
    return 12, &bicycle{} //gown:new                                                    
}

// gown: result 2 iso                                                                    
func gg() (int, int, *bicycle, string) {
    return 1,
        2,
        &bicycle{}, //gown:new                                                          
        "this string is last"
}

// gown: result 3 iso                                                                    
func ggg() (int, int, string, *bicycle) {
    return 1, 2, "new bikes are fun", &bicycle{} //gown:new                              
}

Q2. I don't understand why you declare fmt.Printf to be an observer.  What should be declared an observer and why?

First, did you read the description and current documentation of observers and not understand it? If so, how can it be improved? If not, here is what is in the tutorial to begin with:

README.md line 524:

| `\\\\observer` | designate access (e.g. \rob fmt.Printf) as safe | avoids changing stdlib |

line 654:

## `\\\\observer`

For example, the `\\\\observer fmt.Printf` stand alone comment is used to designate the
debug helpers like fmt.Printf are doing read-only borrows and should not cause alarm.

The observer annotation turns off strict checking on a per-function basis. This is a practical affordance to avoid having to annotate the declarations of the standard "fmt" library.

To summarize, if we do not annotate Printf as an innocuous observer, then it will terminate Gown's proof of for iso uniqueness;

because we cannot otherwise know that it does not store or send away the pointer on a channel.

Since fmt.Printf are frequently used simply for debugging, we do not want the debug prints to accidentally create false alarms about use of iso after proof has been terminated. You can try simply removing the observer annotation to see what Gown reports as an error otherwise. Typically something like:

gown/vectors/ex4/main.go:57:26: GWN008: cannot pass \iso value "a" to untracked parameter
        fmt.Printf("a='%#v'\n", a)

                                ^

On Tuesday, June 9, 2026 at 8:42:50 AM UTC-3 Robert Solomon wrote:

I don't understand why the comment below says "result 0 imm".  Why the 0 in that line?

And, I don't understand why you declare fmt.Printf to be an observer.  What should be declared an observer and why?

//gown: param goner iso; param spare rob; result 0 imm

func puncture(goner *wheel, spare *wheel) *report {}

//gown:observer fmt.Printf
//gown:iso
//gown:clone
//gown:new
//gown:swap

comment branch to attempt to imporove usabilty

That's a typo that should be improve.  

Fixed. Thanks!

[Jason E. Aten]

I have moved the 'comment' branch to master so to update it would suffice to pull down master 

and run make to install or "go install github.com/glycerine/gown/cmd/gown@latest".

[Raffaele Sena]

Maybe I am too late, but I was going to suggest, instead of inventing
a new syntax (while trying to preserving the original for .gown files)
you could do something like this:

//gown: func newTicket(name string) \iso *ticket
func newTicket(name string) *ticket {
...
}

Maybe it's a little too verbose, but it makes clear what you are doing

On Tue, Jun 9, 2026 at 11:10 AM Jason E. Aten <j.e....@gmail.com> wrote:
>
> I have moved the 'comment' branch to master so to update it would suffice to pull down master
> and run make to install or "go install github.com/glycerine/gown/cmd/gown@latest".
>
>
>

> --
> You received this message because you are subscribed to the Google Groups "golang-nuts" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/golang-nuts/815ee960-0a87-44a7-b5d7-1e0faa45da6fn%40googlegroups.com.

[thepud...@gmail.com]

Hi Jason,

gown looks very interesting!

One initial question I have is whether or not it would be appropriate for it to be a static analyzer rather than a pre-processor (currently doing source-to-source transformation)?

Maybe the changes in your new comment branch essentially make it a static analyzer? If so, it might be beneficial to describe gown in general as a static analyzer (even if it does source-to-source transformation under the covers for now).

Also, good chance you are already familiar with this, but I thought I'd briefly mention 'checklocks' from the gvisor project as some possibly related prior art that might be worth a look:
    https://github.com/google/gvisor/tree/master/tools/checklocks

Three things from there that spring to mind that might be related to your work:

 1. checklocks could be an example of comment-based annotations that you might draw inspiration from.
 2. checklocks is set up as an analyzer that works with 'go vet' and the x/tools analysis framework, which usually has some advantages like better performance and being more inter-operable and so on:
    https://github.com/google/gvisor/blob/master/tools/checklocks/checklocks.go#L40
 3. checklocks has some basic ability to suggest annotations automatically, and I wonder if something like that could make sense for gown (if it does not already do so):
    https://github.com/google/gvisor/blob/master/tools/checklocks/analysis.go#L899-L905

Looking just now, I also see a checklocks demo repo that might be worth a read (put together by an external Go contributor I think):
    https://github.com/kakkoyun/checklocks-demo

Finally, one other bit of food for thought might be how gown could possibly use typed struct annotations in the future, which sounds like it could be plausible based on some of the json/v2 discussions:
    #74472 -- "proposal: spec: typed struct tags"
    https://github.com/golang/go/issues/74472
 
Sorry if some or all of that is off base.

In any event, very interesting work!

Best regards,
--thepudds

[Jason E. Aten]

Ah nice, Raffaele! I like this idea. I think it is actually clearer than my current "comment" syntax. I need to go read the other prior work that thepudds mentioned too, but I'll probably revise towards your suggestion, since it seems clearer to me.

[Jason E. Aten]

Hi thepudds,

thanks for the interest and the pointers. Your comments are very on point. 

It would be fair to call gown a static analyzer, sure. It does alot of heavy

lifting to locate where the ownerstamps are before erasure and package loading,

so I'm not sure the current vet analysis frameworks would help, but I'll look

into them. 

https://github.com/viperproject/gobra is pretty heavy weight and

takes alot more annotation than Gown, but also proves alot more (if you're

willing to load up their JVM based checker and write alot more invariants).

Gown is much lighter and much more focused on the channel transfer of ownership since that seems 

under served by the race detector.

I'll have to take a look at checklocks in more detail. Thanks for the suggestion!

Best wishes,

Jason

p.s. Raffaele your suggestion for function annotation in //gown comments is now implemented.