Why is that? And what alternative do you prefer? I do not mind it for what it is meant for. I rather would have it more practical (instead of having to write software twice: once to prove it and once to execute it), but that is also very new and experimental, like F* or Idris.