The verification is, which allows the optimisation to be extremely broad and non deterministic.
It's really unlike a compiler. For example, for a function like 'sort', the optimisation can:
- Use quicksort if the data distribution is generic.
- Use insertion sort if the data is nearly sorted
And so on... As long as these can be proven sound, Maxwell can pick the best optimisation in real time.