Currently, all our haskell returns IO T, which means that functions which could be considered pure, are not. It would be quite valuable if we added support for this, as that further improves ergonomics.
There are three mechanisms I see:
- All
const fn functions could be treated as implicitly pure (I believe).
- It could be a cool idea to integrate with Creusot.
- We could, of course, add our own
#[function(pure)] annotation.
Currently, all our haskell returns
IO T, which means that functions which could be considered pure, are not. It would be quite valuable if we added support for this, as that further improves ergonomics.There are three mechanisms I see:
const fnfunctions could be treated as implicitly pure (I believe).#[function(pure)]annotation.