The goal (as I understand) is to create a new kernel to serve as an underlying layer below the "user-space" part of Fixpoint.
The ultimate goal would be to enable an API call to generate a Fix object that represents a serializable continuation of the current procedure from wherever the API function was called. This continuation would behave like any other Fix procedure (i.e. it could run anywhere and be assured of producing the same output).
Another benefit would be letting us avoid having custom patches to lld...
The goal (as I understand) is to create a new kernel to serve as an underlying layer below the "user-space" part of Fixpoint.
The ultimate goal would be to enable an API call to generate a Fix object that represents a serializable continuation of the current procedure from wherever the API function was called. This continuation would behave like any other Fix procedure (i.e. it could run anywhere and be assured of producing the same output).
Another benefit would be letting us avoid having custom patches to lld...