← Back to context Comment by igravious 2 months ago i'm doing the same thing but for type theory 3 comments igravious Reply potsandpans 2 months ago This is very interesting to me. Care to share your process? igravious 2 months ago one agent to write the C code, one agent to write the Agda code, and an agent to bridge the two and make sure that the C code does what the Agda code says it does.https://gitlab.com/igravious/lettuce.git potsandpans 2 months ago Sounds cool. Your repo might be private, I can't view it.
potsandpans 2 months ago This is very interesting to me. Care to share your process? igravious 2 months ago one agent to write the C code, one agent to write the Agda code, and an agent to bridge the two and make sure that the C code does what the Agda code says it does.https://gitlab.com/igravious/lettuce.git potsandpans 2 months ago Sounds cool. Your repo might be private, I can't view it.
igravious 2 months ago one agent to write the C code, one agent to write the Agda code, and an agent to bridge the two and make sure that the C code does what the Agda code says it does.https://gitlab.com/igravious/lettuce.git potsandpans 2 months ago Sounds cool. Your repo might be private, I can't view it.
This is very interesting to me. Care to share your process?
one agent to write the C code, one agent to write the Agda code, and an agent to bridge the two and make sure that the C code does what the Agda code says it does.
https://gitlab.com/igravious/lettuce.git
Sounds cool. Your repo might be private, I can't view it.