7 ms·

I think formal verification makes sense for programs like optimising compilers. You have a reasonable hypothesis to prove: That the optimisations don't change t

I think formal verification makes sense for programs like optimising compilers. You have a reasonable hypothesis to prove: That the optimisations don't change the behaviour of the program in any way, except for speed.

astrange 5y ago
It's not "in any way" but "in any way we care about" - people love optimizations like -ffast-math that are not well founded.