> Using a mode checker on existing software is unproductive, but rewriting existing, working software that you have to shoehorn into a shape rustc .... will compile is productive?
The rewrite is a 1-time cost.
> Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not?
I am primarily a Haskell user, and I already said I have nothing against GC. Those other languages (except for F#) are great!
> has no specifications or alternative implementations
That is a major downside (I work on GHC and wish it wasn't the only game in town) and affects all of those. That's why I put out SML and the CakeML implementation. SML lacks shiny new stuff but the grunt work has been done.
I would certainly use SML over any variant of C for anything that needs dynamic allocation.
The rewrite is a 1-time cost.
> Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not?
I am primarily a Haskell user, and I already said I have nothing against GC. Those other languages (except for F#) are great!
> has no specifications or alternative implementations
That is a major downside (I work on GHC and wish it wasn't the only game in town) and affects all of those. That's why I put out SML and the CakeML implementation. SML lacks shiny new stuff but the grunt work has been done.
I would certainly use SML over any variant of C for anything that needs dynamic allocation.