at least with what i have seen of program synthesis, you end up having to write such a specific specification that you are basically defining the implementation

at least with what i have seen of program synthesis, you end up having to write such a specific specification that you are basically defining the implementation (i.e., programming). dependently typed languages also seem woefully unprepared for real systems programming. they are probably good in the small but are so difficult in the large that the costs outweigh the benefits.