Can signatures be made simpler and error messages be made better?

[Ola Fosheim Grøstad]

On Saturday, 12 June 2021 at 11:14:08 UTC, sighoya wrote:
> Just to reiterate the essence: The general problem with static 
> dependent typing is to track type (lifetime) state to make the 
> lifetime constraints useful, otherwise you have hard times to 
> auto prove your code given the life times constraints.

Not really sure what you mean now. You would have to make the 
constraints more limiting than needed, to get the verification to 
pass. That is certain.

However, the basic idea would be to emit the high level IR, so 
there is really no limit to what can be analyzed.

> It is true that we would save lifetime inference if we would 
> make it as an opt-in.

I don't think it should be opt-in. The code gen would optimize 
based on the guarantees that are stated in the code. So the 
verfication would run, but it could run delayed, then feed back 
information to the IDE.

I think it should ship with the compiler, but I think it should 
be a separate pass.

It can be done as a separate program for sure. Which also would 
allow using solvers developed for other languages.

Start thinking of D-tooling as a set of tools, not just DMD. So 
you have DMD + verifier + IDE-server + IDE of you own choice.


> I think, this is the reason why Rust makes it mandatory all the 
> time.

Maybe the mindset of Go and Rust teams are very conservative and 
stuck in the past?

Try to think of the compiler as just a small piece of the 
development environment.