3 ms·
A shot in the dark: it could perhaps help in automatically optimizing algorithms by proving that the optimized version is equal to an easily written and reasone
by ganzuul 7y ago
A shot in the dark: it could perhaps help in automatically optimizing algorithms by proving that the optimized version is equal to an easily written and reasoned about.
- Labo333 7y agoI think reasoning about correctness is easier than about optimizations. Even if you account for a simple complexity model (real computers are a lot more complex, because of techniques like branch prediction or memory caching), proving an implementation as optimal is very hard!
- hwayne 7y agoIt's often really hard to know if an optimization is "correct"- is the same function as the original, unoptimized version. Formal methods helps here by showing they're equivalent, so you can focus on finding good optimizations instead!