3 ms·
> Write a type declaration for a function with an expressive type system, e.g. refinement types. Then use LLMs + SAT/SMT to generate provably correct code. Thi
by amiantos 3y ago
> Write a type declaration for a function with an expressive type system, e.g. refinement types. Then use LLMs + SAT/SMT to generate provably correct code.
This is how I use copilot currently, so I might not be following on what part of this is 'future' facing or relevant to this Fructose project?
Not being contrarian, I thought this was an interesting point but as I thought about it more I realized, "wait, they're describing what I already do".
- AgentOrange1234 3y agoHow do you do this? I know nothing but this sounds really interesting.
- nextos 3y agoDo you use Copilot on a language equipped with refinement or dependent types, and use said types to constrain generation of entire functions, in a single step, that are also formally verified?
- trenchgun 3y agoHow!!! Could you think of writing a blog post about it?