4 ms·
And in the functional world, Lean 4 achieves language level support for local mutation, early return, etc. in the same way, by converting it into non-mutating c
by nequo 2y ago
And in the functional world, Lean 4 achieves language level support for local mutation, early return, etc. in the same way, by converting it into non-mutating code:
https://dl.acm.org/doi/10.1145/3547640 https://dl.acm.org/doi/10.1145/3547640
- p_l 2y agoIn some ways, CPS as compilation target already went that way. Sure, ultimately the code mutates values in place, but the specific actions are modeled as pure operations