I think it's harder to find an error in a program than in a proof. At least for proofs that can be verified automatically by a computer. And that scales with th

I think it's harder to find an error in a program than in a proof. At least for proofs that can be verified automatically by a computer. And that scales with the difficulty of the problem. A proof that a program copies files from one place to another is not interesting. However a proof that your algorithm can safely share state without a lock is. My point here is not that dependent type theory is going to take over the industry and we should all learn to write proofs! It's more that we can if we want to. Writing a proof with tactics in Lean feels a lot like programming with typed holes in Haskell (it's harder but the experience is similar). With training a motivated programmer can write proofs that verify their designs which provide a strong guarantee of correctness. Whether types are more expressive than programs... I think they are? That seems to be the whole point of Synquid: you can express complex constraints and proofs in your types that enable it to derive the program for you. Is that easier than simply writing the program? I think one should consider that writing the correct program is harder. And where getting it right matters a lot I hope that synthesis will one day allow us to derive those programs from their specifications (or at least the parts that matter the most). It would save a lot of the burden of proving that the program we wrote implements the specifications.