goose
goose copied to clipboard
tchajed
Goose converts a small subset of Go to Coq
Hi, I am not sure if it is intended to capture the recursive function translations, but Goose can translate the recursive function in a format that you cannot load it...
For control flow and assignments, it would be conceptually clearer if we supported them by rewriting the AST to satisfy some invariant and then translating the result. For example, this...
Go has an (unusual) feature of infinite-precision computation of constant integer expressions, which are formally considered untyped in the language. Goose does not support untyped constants (which would be modeled...
Right now we write code like ``` type foo struct { bar *Bar } func (f *foo) UseBar() { f.bar.DoSomething() } ``` This results in double dereferencing - once to...
Hi, I'm happy to help out wherever I can, but I'd love for interfaces to work. I propose that for an initial iteration, only closed interfaces are supported (i.e. interfaces...
Converting `len` to `uint32` via a type wrapper is mistranslated, dropping the type wrapper and using `slice.len` (which produces a `u64`). ```go type Uint32 uint32 func failing_testU32NewtypeLen() bool { s...
Hi, I have a quick question. As far as I understand, goose can generate gooselang version of the following type A struct { a uint64 b *B } type B...
Rather than translate `const` declarations to global expressions, we should try to translate them to their value in `Z` and then use them as `#ConstName`. We would probably not bother...
In `for...range` loops over a map, we should support `break` similar to how ordinary `for` loops work. The concrete use case is code that finds an arbitrary element in a...
Goose doesn't yet support receiver methods for non-struct types. However, it's probably bad UX to panic (without saying the unsupported error msg), like it does in this example. ```go type...
