Re:Please do not attempt to simplify this code
by AstralStorm on Friday December 28, 2018 @04:30AM
(#18775777)
Compilers and libraries are written by humans and are probably the most fallible things ever, optimization wise. I'm not talking 1% here. I'd love to see an opposing compiler with an automated proof that it does what it claims.
Well, unless your computer can read and parse high order proofs over code. Not even Haskell can do that. (It can barely parse F types much less optimize them.) The closest I have come to that feature is Isabelle's simplify and even that is limited.
GCC and Clang can do basic bounds proofs at best and otherwise are tough buggy heuristic beasts. Just look at the trackers.
GHC has a slightly easier job but it's paid for in programming complexity. There are hoops in type system you have to jump to get performant code... and even then the code generated its at best meh quality. There is always some joker telling that it could be compiled for SIMD or multithreaded but that never materialized in usable form.
Well, unless your computer can read and parse high order proofs over code. Not even Haskell can do that. (It can barely parse F types much less optimize them.) The closest I have come to that feature is Isabelle's simplify and even that is limited.
GCC and Clang can do basic bounds proofs at best and otherwise are tough buggy heuristic beasts. Just look at the trackers.
GHC has a slightly easier job but it's paid for in programming complexity. There are hoops in type system you have to jump to get performant code... and even then the code generated its at best meh quality. There is always some joker telling that it could be compiled for SIMD or multithreaded but that never materialized in usable form.