Programming is isomorphic to theorem proving (according to Curry-Howard).
Therefore trying to estimate a software project is a bit like trying to estimate how long it will take to prove a new theorem in mathematics, assuming you would know which exact theorem you want to prove.
In a way I think yes but just getting the type-check right would be like proving ANY mathematical theorem. It is very easy to prove mathematical theorems if you don't care what those theorems are.
The challenge in mathematics, and programming, I believe, is what ("lemmas") to prove so that you can then prove more things that are useful for engineering, science, etc. . What functions to write in your program so that you can get its "main function" to do something useful.
Add to that the fact that much of the "type-checking" with current practical programming languages still has to be done informally, to describe what we expect of the result and then prove (to yourself and the client) that the program does that.
A lot of the thought-process that goes on in programmers' heads is informal reasoning proving things to yourself, "If I make this change here then that thing there must have a correct value, and then ..."
Therefore trying to estimate a software project is a bit like trying to estimate how long it will take to prove a new theorem in mathematics, assuming you would know which exact theorem you want to prove.