[syrak]

> In this case it is hard to be sure that the function must behave in the correct way because of its type.

I would argue that in this case it is quite easy to ensure that it does the right thing, because even if the implementation is not unique, the number of possibilities is extremely limited. In the case of `Put` you can return either the new state or the old one. It takes a single unit test to ensure it's putting the new one, with parametricity to generalize from one case to all cases, still without looking at the implementation.

> In the second case, why do we have a program at all? If there is only one correct program we could have written then it seems to me that the program is in fact the type and the compiler ought to have been more clever and written it itself. (There are of course plenty of issues with that statement).

Program synthesis being basically proof search, even after the right automation is developed it may still be more practical to write the program by hand.

> They are particularly useful in proof assistants like Agda where one must manually exhibit a million trivial propositions and holes help fill in all the boring gaps.

I think the same mechanisms and benefits are at play here in a non-dependently-typed setting, even considering "entirely writing a function for you" as an unwarranted exaggeration.