> 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".
Do 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?
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".