[choeger]

> Some people judge the language on their ability to get work done with it.

Really? Safety and correctness aren't relevant for you? Then why even bother with go instead of Python or a Lisp?

For me it's crucial that a programming language contains tools that allow me to definitely rule out as many errors as possible. A powerful (and sound) typesystem does just that.

[ori_b]

How are you finding Idris? or are you more in the Agda camp?

If you want to definitely rule out as many errors as possible, dependently typed languages are the state of the art, allowing you to write a sort function that will fail to compile if it returns a list that isn't sorted (eg,https://dafoster.net/articles/2015/02/27/proof-terms-in-idri..., or https://www.twanvl.nl/blog/agda/sorting).

After all, if you can't even prove basic properties about your code from your language, like array accesses being within bounds, are you really using all possible tools to rule out errors at your disposal?

[choeger]

To be fair, I never had a chance to use Idris nor Agda. I don't know how capable I would be to encode the proofs in libraries nor client code. If it's usable, I am all for it.

Otoh, I do know that languages like OCaml, Haskell, or Rust take the burden of trivial errors from my shoulders for neglible cost.

[eyelidlessness]

Yeah, that was an insincere gotcha question, and it's a shame that it could potentially undermine other readers' potential value of a higher degree of confidence versus a hypothetically perfect confidence.

[grey-area]

Does Rust also have a feature that instills a burning desire to proselytise?

[choeger]

I like Rust mostly for its user-friendly tools. I dislike the compilation model. The type system I already liked even before Rust existed. So, not every String opinion on PL is down to Rust.

[5e92cb50239222b]

No, I just find discussions like these absolutely hilarious. A Go developer with ten years of experience convinces himself that Go is the gospel and generics are a useless toy and distraction from "real work™", then tries generics and they move from a feature you don't really need to a feature you couldn't possibly live without.

Same with every other thing that goes into this language. A thing that's been available elsewhere for literally 3-4 decades.

We have some examples in this very thread.

[grey-area]

Your description doesn’t match what I see in this thread at all.

Odd that you’re so upset by other people’s choices.

[lenkite]

Yes, all Rust devs get infected with the PROSELTIZE virus. Other languages are desperately trying to develop vaccines.

[AnimalMuppet]

> > Some people judge the language on their ability to get work done with it.

> Really? Safety and correctness aren't relevant for you? Then why even bother with go instead of Python or a Lisp?

A charitable reading of the GP would be that "safety and correctness" would be included in "getting work done", in amounts that are appropriate to the work in question. Your interpretation is... less than charitable.

[LanceH]

Exactly. Go is safe enough. Correctness for most programs is more about making sure it solves the problem correctly, not merely that it guarantees no errors if it runs. That feels like a modern version of "It compiles, I'm done."

[fnord123]

Maybe they don't want a target directory using 3gb from a clean build.

[cloudfifty]

It's already self-evident that Go manages that just fine. That's just weird dogma.