grumpyprole

It was indeed a big yak to shave. Cloning a Microsoft technology probably wasn't a good idea for OSS adoption either.

Lol, I like the word "metalness".

The Xerox Alto was early 70's and that GUI OS was written in Pascal. I always thought Pascal was better designed and less bizarre than C. Null terminated strings were particularly a bad idea.

I've seen C++ systems that are considerably slower than equivalent Java systems, despite the lack of stack allocation and boxing in Java. It's mostly throughput, malloc is slow, the C++ smart pointers cause memory barriers and the heap fragments. Memory management for complex applications is hard and the GC often gives better results.

> Also, compilers don't reason about code the same way humans do.

Not these compilers for sure. But I don't agree that all compilers are broken.

> They apply a large number of small transformations, each of these transformations is very reasonable and it is their combination that results in "absurd" optimization results.

Humans use techniques like natural deduction to apply a series of transformations that do not lead to absurd results.

IIRC, Mac OS Classic was written in Pascal, as were other operating systems. C just won the popularity contest.

It could be more performant because of the known constraints around it, or it could be an ad-hoc, informally-specified, bug-ridden, slow implementation of half of some data structure. At least with a generic and resuable data structure you have a known reliable building block. Again, performance over safety.

The technical arguments should be obvious, e.g. spending ones complexity budget on manual memory management and avoiding footguns. But one amusing anecdote is that the open source GNOME project founders were so traumatized by their experience building complex GUI apps in C (already a dubious idea 20 years ago), that they started building a C# compiler and the Mono project was born.

+1. Part of the problem is that x86 assembly is hardly programming the metal anymore. The performance characteristics of processors has changed over the years also, compilers can be more up-to-date than humans.

Just an old name for a portfolio of transactions

This is FUD. You don't need to have studied abstract algebra to understand the monad laws. Basic high school maths is more then sufficient.

EDIT: Apologies, I missed the subtle point this post was making!

> I don't give a shit what languages CAN do in theory.

Then I'm sure you'll be very satisfied with languages like Go and Zig. I am not satisfied with them, because I know what can be done.

> You brought up linters. Not me.

I did not. They were brought up by others as apparently one way that Go programmers work around lack of sum types.

> There's no type annotations for me to figure out what the heck each term is

You can add additional annotations in OCaml if you want, or just query the type of a term in Merlin.

> a compiler with thousands of lines that I navigate with an IDE, with logging, with annoying little edge cases, with dozens of collaborators, I'd choose Rust.

Why? OCaml supports logging and IDEs. Simple elegant code without the burden of manual memory management, makes it better able to cope with edge cases, being taken apart and refactored etc. Less of the complexity budget has already been spent.

> It's an example of what Haskell's IO API might look like if it used sum types for error handling rather than throwing exceptions.

Apologies I missed that bit, it is indeed a perfectly reasonable API.

> So you're saying that you'd configure the compiler to do exactly the same checks that Go error linters do...none of which have anything to do with sum types.

We are arguing semantics as to what constitutes a "handled error". If a user chooses to explicitly throw away the error and not use the value, then you are arguing it is not handled. I am arguing that it has been handled (and checked as such). Either way sum types are a step in the right direction, despite all the shortcomings and unsound type systems of "practical" languages.

> No. I said nothing about null safety. What I said is that “sum types by themselves do nothing to force handling of errors”.

Maybe (null) types are the simplest form of error type, with null pointer exceptions being the simplest from of unhandled error. They are therefore the easiest example to illustrate my point. You cannot simply choose to ignore them and remain credible. Haskell's broken old IO APIs are hardly a model example. Your Haskell code will at least give a compiler warning for ignoring the output. I would configure the compiler to turn this into an error.

> Sum types by themselves do nothing to force handling of errors,

If you have Haskell experience, then have you ever wondered how it is considered "null safe" and does not throw null pointer exceptions? Perhaps it is because optional "Maybe" types (the simplest form of error) must be explicitly unpacked? Yes, Haskell, being an old language without a sound type system, permits "fromJust" and its exceptions (a side effect) are not tracked like other effects. But despite this, are you seriously claiming that sum types "do nothing" to achieve this null safety?

If you want to understand the full proving power of sum types, I do not suggest Rust or Haskell as a model example. Coq, Agda, Idris or ATS will be better examples.

> All do

No, this is not true. A total functional programming language can disallow partial functions that circumvent the type checker.

Again, linters only get you so far. For example, sum types eradicate null pointer exceptions, linters do not.

> but also seem to erroneously suggest that Rust’s type system somehow can.

I didn't bring Rust into this discussion, it is hardly a model implementation of sum types and using them for proofs, but it is certainly a step in the right direction.

> My issue here is not with the utility of sum types, but with the erroneous claim that they somehow remove the need for linters or compiler warnings

You are misrepresenting my posts, I am responding to an erroneous claim that linters are a satisfactory substitute for sum types.

Unwrap and fromJust can be disallowed if need be, they are "unsafe" convenience functions whose use can and should be tracked. Not all languages with sum types will permit them. Rust also has "unsafe" code blocks, should we also claim it is therefore not memory safe? Some would try to do so, but at least this unsafe code is tracked and not idiomatic.

> programming languages are not mathematics

This may be how you choose to view them. But many of us seeking to build safer and more correct software aim to make programming more like mathematics. Mathematics tells us how to compose and tells us how to prove. Both things the software industry is currently failing at.

> only enforces the rather weak constraint that you cannot access a non-error return value in the case where the function returns an error.

This "rather weak constraint" as you put it, completely solves Tony Hoare's "billion dollar mistake": null pointer exceptions. Something Go also suffers from due to lack of Sum types. With regard to your Rust example, the compiler will give a warning that can be turned into an error to completely prevent this, if desired.

As the parent said, sum types are "foundational" and have many applications for writing safe statically checked code. Eradicating null pointers and enabling chainable result types are only the tip of the iceberg.

> no chance of forgetting to check the error, and works just as well as a stronger type system

A linter-based syntactic check is no substitute for a proper type system. A type system gives a machine checked proof. A heuristic catches some but not all failures to handle errors, it will also give false positives.

A simple syntactic check will only ever work as a heuristic. Heuristics don't work for all cases and can be noisy. The point is, no modern language should need such hacks. This problem was completely solved in the 70s with sum types.

Go's lack of sum types mean that there is no static check for whether the error has actually been handled or not. Go's designers went to all the trouble of having a static type system, but then failed to properly reap the benefits. Sum types are the mathematical dual of product types. It makes sense for any modern language to include them.

I also thought checked exceptions in Java were fantastic. They are a form of statically checked effects. I would like to see more of this sort of thing not less.

Why is JS even relevant to this discussion?

And this attitude is why it's a serious issue in our industry. You clearly don't take security seriously, to the point that it's a laughing matter for you.

Yes Ada/SPARK is a great example.

You might think that, if you live in a small world. I want memory safety, but I am otherwise not a big fan of Rust. Rust tries to be too high-level like C++, making it opaque where allocations are happening. For a low-level systems language, with embedded proofs, I quite like ATS, but Vale is also promising and more like Zig.

> At some level you need languages that are not “memory safe”.

Perhaps as an escape hatch (unsafe Rust) or a compiler target, but ideally not as a "general purpose language" as Zig is marketed as.

Maybe doing it for new projects is better than doing nothing?