I discovered the power of loop invariants during a course at university. A professor even developed a compiler like this, starting by defining invariants and wr

I discovered the power of loop invariants during a course at university. A professor even developed a compiler like this, starting by defining invariants and writing the code accordingly. Really inspiring! I wonder, are there such techniques tailored to functional programming? (immutability, recursion,...)