[killin_dan]

Funny enough, I think you've actually hit the nail on hm the head about what makes go programmers so irritating, that they think the go spec has somehow taken into account "the right way" for every possible problem. It's so obnoxious.

Problems that actually matter is such a good indicator that someone has no idea what they're talking about.

Formalization and proofing is what MATTERS. If you ain't got that, you're basically just guessing

[shakna]

> Formalization and proofing is what MATTERS. If you ain't got that, you're basically just guessing

And that's what makes Haskell evangelists intolerable. (Even if Haskell isn't your favourite language).

Go has it's place.

C has it too, especially on devices with > 32kb memory.

I adore Scheme and it's spec, it's expressiveness, and flexibility. Doesn't mean I think it's the best language for running a game engine, though it has been done.

We all have reasons we like our languages, and what they can be, and what they're good for.

But no language is the be-all, and end-all, of languages. There are always trade-offs. It just can't be helped.

Awk is amazing at dealing with small bits of information, quickly. It's a full language, that has been used to write some large programs... But it isn't as well suited to that. As a scripting language however, it's great.

Python is my go-to for prototyping. It can be a tad inconsistent, and more verbose than my tastes, and weaker typing than I'd like, but it works well enough.

Can't we all just get along?

[jfoutz]

C is glorious. After a bunch of years screwing around with a bunch of different languages, I believe popularity is an indicator of local optima. C hit so many important points, it became critical. I think it blew its competition away, 40 years ago.

Go people have a point. Haskell people have a point. Their points aren't as strong as c's was, back in the day, so they don't dominate in the way c did.

We don't have a clear winner right now. Different languages bring different things. We are in another exploration phase of languages.

[shakna]

C has so many decisions that feel odd, but make so much sense! (Yes, I love C).

I'm in the process of building a tiny programming language for some Arduinos, as part of a homebrew computer.

I'm making the memory space as a stack.

But how to have a variable know it's location in the stack?

Return an int! Oh, I just reinvented the typeless pointer C has.

PLT exploration is fun, exciting, and love reading about experiments like Magpie and Wren.

But... I still use C99 at work every day, and there's nothing wrong with that.

[Insanity]

> C has it too, especially on devices with > 32kb memory.

Can I assume you mean, devices with < 32kb memory? Or is there another language you would use on devices with such as small amount of memory instead of C?

[adrianratnapala]

The local assembler? Fortran? Forth?

Personally I would prefer C. But I can see arguments for each of the above.

[shakna]

Sorry, less than.

100 > 32.

[cle]

> Formalization and proofing is what MATTERS. If you ain't got that, you're basically just guessing.

You're guessing either way. By formalizing and using deductive proof on those forms, you're guessing that your forms correctly model the intended behavior, which gets harder as the forms get more powerful and abstract. You can 100% guarantee the properties that follow from the forms. You can't deductively prove that your forms are the right forms, and that becomes more important--and harder to verify--as the forms get more abstract and powerful.

Which is what irritates me about static typing zealots. Static typing is useful in that it provides deductive guarantees, but it's not free and does have tradeoffs and pitfalls. Instead of requiring 100% guarantees of correctness, you can relax it and require sufficient guarantees of correctness, which will enable you to use the same mechanisms to inductively prove more useful things more easily, and allow you to use the same mechanisms to verify more assumptions and properties than is reasonably possible with formal verification. That's a tradeoff that should be considered more often than it is.

A primitive example of this is the use of unit tests to replace some of the formal proofs done by type checkers. There are undervalued advantages to writing programs that way--leaning on inductive instead of deductive guarantees of correctness.

[marcosdumay]

The point of a type system is 100% guarantees. Honestly, if it fails at that, I'm not sure it becomes useful at all for correctness (it may still be useful for operation overloading).

Now, of course, nearly all systems have many properties that you don't want to enforce by the type system. Proofs are hard work, better do them only where it's easiest or really important.

Yet, most times I hear the phrase "static typing zealots", it comes from somebody that does not have experience with a good type system and is thus completely unable to weight off the work of constructing your types and the one of getting enough tests to be sure your program works.

[AnimalMuppet]

> Problems that actually matter is such a good indicator that someone has no idea what they're talking about.

> Formalization and proofing is what MATTERS. If you ain't got that, you're basically just guessing

This is how you become irrelevant. "Problems that actually matter" are the problems that actually matter - matter to the people who are trying to write programs. If you're trying to write proofs, then formalizing and proofing matter. More of us are trying to write programs, though.

[Risord]

I think "proof" shouldn't be taken too literally. At the end stronger type system make easier to craft correctly working programs and less lottery machines.