catnaroek

The problem with Ada isn't that it's niche. The problem is that it has a gazillion features whose purpose is (ostensibly) to make programming errors easy to prevent, identify and correct, but fail miserably at it. There is more to programming than safety, but if safety is going to be one of your programming language's selling points, then the least you can do is get it right. The process for getting it right consists of the following steps:

(0) Identify a concrete class X of programming errors you want to eradicate.

(1) Postulate a mathematical theory of what it means for a program not to have errors of class X.

(2) Develop proof techniques that are powerful enough to establish that “interesting” programs do not have errors of class X.

(3) Design algorithms that use these proof techniques to prove, or at least validate a purported proof, that a program does not have errors of class X. Your algorithm must be able to analyze program fragments (modules, classes, whatever) independently, and combine information obtained from several program fragments without reanalyzing them from scratch.

Safety can be established in three ways:

(0) Automatically and statically, in which case there is an unavoidable tradeoff between the simplicity and the power of the static analyses. Example: non-lexical lifetimes.

(1) Automatically and dynamically, in which case you need performance-draining checks. Example: slice indexing.

(2) Manually, i.e., leave it as an exercise for the programmer, in which case you need a language with a formal semantics, because how else are you supposed to prove anything? Example: none that I know of in Rust or any other similar language.

There are no other options, although you can take a pick and choose approach for different use cases. IMO (2) has not been given the attention it deserves.

---

So, do you have any concrete idea regarding what could be made simpler?

It took me half a minute to just parse the title.

Edit: I mean the title of this post here. The title of the linked article is, of course, very easy to read.

A Go interface type is not an abstract data type. The difference is not even subtle:

(0) An ADT has a single internal representation that is known to the implementor, but hidden from users. The upside is that the ADT implementor can use his knowledge of the representation to optimize on n-ary operations, i.e., operations that act on several instances of the ADT. The downside is that ADTs cannot be extended by third parties. You would have to create a different ADT, even if satisfies the same contract.

(1) A Go interface has a list of methods, but does not proscribe any fixed internal representation. The upside is that anyone can create values of an interface type as long as they can implement the methods. The downside is that it is difficult to implement n-ary operations, because, at any point in the program, the implementor only knows the internal representation of the single value they are currently creating.

In other words, ADTs optimize for efficiency and predictability, whereas interfaces optimize for flexibility and extensibility. As a general rule, ADTs require more time than interfaces to plan ahead their design and implementation, but already implemented ADTs are easier to use correctly than already implemented interfaces.

> Abstract data types are designed specifically for data structures like queues and stacks

Guess what all nontrivial programs manipulate in the end.

> objects that don’t have such well defined invariants

... are either stateless or useless. It is impossible to define useful algorithms that manipulate objects of which you cannot say anything.

> No major language has adopted them for that reason.

The real reason is “programmers cannot reason about invariants anyway”.

If you want data abstraction to do at least a minimum of static invariant enforcement, you pretty much have to use abstract data types. But if you're fine with littering logs with “exception was caught here, such and such data structure was corrupted”, suit yourself.

Abstract data types have nothing to do with either algebraic data types or abstract classes.

> Most interfaces have one implementation. Instead, they are about abstraction, design, and so on.

Then what you want is an abstract data type. Unlike interfaces, which can be implemented anywhere, an abstract data type is implemented in a single place. This has obvious benefits for performance (clients don't need to dynamically dispatch on operations), control (implementors don't need to worry about malicious clients supplying impostors) and precision (a single module can export several abstract types, whose implementations are mutually dependent).

Go's interfaces are pretty terrible at all of the above. Not that Java provides anything substantially better.

It's no less immoral in programming languages than in real life, precisely because it tends to slip from the former into the latter.

It is programmed by humans. Machine learning algorithms are designed and implemented by humans. If machine learning algorithms do not perform well in a way that puts human lives at risk, the humans who designed and implemented them are responsible.

How shallow are the books that the author of this piece reads, that he can keep their entire contents in his head? I am pretty sure I can't keep the entire contents of my personal library in my head. And I don't even have that many books. (Around 20, between CS and math books.)

> This is a collection of topics that you wouldn't ordinarily find in undergraduate math classes.

Much of this course is covered in undergraduate math classes, except at much greater depth (especially algebra and probability theory), and over the span of several courses.

The original post to which you replied begins with:

> As I said before, resource management is first and foremost a matter of correctness, so performance is neither here nor there.

Your proposed alternatives, namely:

> In Modula-3 or D, as possible examples, a solution might be destructors or scope attributes.

merely offer automation, not verification. Automation without verification simply makes screw-ups harder to undo.

> Abstract data type inheritance is about substitution: this thing behaves in all the ways that thing does and has this behaviour (this is the Liskov substitution principle)

There is no such thing as “inheritance” for abstract data types, because inheritance is a syntactic relation between two definitions (which needn't be type defintions, by the way!). Abstract data types may be related by subtyping, although IMO this is hardly ever useful. What you actually want to refine is abstractions (of which abstract types are merely constituent parts).

> As a type, this relationship is reversed: you can use a rectangle everywhere you can use a square (by having a rectangle with the same width and height), but you cannot use a square everywhere you can use a rectangle (for example, you can’t give it a different width and height). Notice that this is incompatibility between the inheritance directions of the geometric properties and the abstract data type properties of squares and rectangles; two dimensions which are completely unrelated to each other and indeed to any form of software implementation.

There are valid arguments against inheritance, but this is not one. In fact, this argument has nothing to do with inheritance at all! All that this says is “if the type variable T only appears in contravariant position in F(T), and A is a subtype of B, then F(B) is a subtype of F(A)”. Moreover, this is not an argument against subtyping either. It's just the description of how to handle it correctly. It appears in any standard PL semantics or type theory textbook.

Here is a real argument against inheritance: “Try formalizing the semantics of a toy language with inheritance. Try proving things about a couple toy programs using this semantics. Note how the proofs about what your superclasses do often make a lot of unwarranted assumptions about how subclasses will use or override inherited functionality. These assumptions couple not only the interfaces (which is okay), but also the implementations (which is not okay) of superclasses and subclasses. This is the antithesis of modularity.”

> Memory safety almost always involves some type of runtime checks: even memory safe languages usually (always?) have runtime checking of array bounds, for example.

Indeed, array manipulation is completely unsafe in most languages, as array indices are effectively unityped. (This may be a unitype of everything, as in Python, or a unitype of indices for all arrays, as in Java or ML.) There are several ways to fix this issue, with various tradeoffs between convenience and expressive power. None of them has become mainstream, but it's good to remember that they do exist.

> So it's understood that a memory safe language will generally be composed of syntactic and semantic features which help at compile time, and runtime checks to close any remaining holes.

Safety is any means by which you can establish that every operation a program may perform is meaningful. Now, I don't know about you, but at least to me, it is never meaningful to dereference an invalid pointer or use an invalid array index. Whether the error is trapped at runtime is neither here nor there.

In the presence of reference-counted mutable objects, destructors no longer guarantee that cleanup will happen. But that much is okay. This is a liveness property, and, as far as I can tell, nobody really knows of any non-annoying way to enforce liveness properties with types. On the other hand, “cleanup is the last operation that can be performed on an object” is a safety property, and types are excellent tools for verifying properties of this kind.

> where you've basically created a c++ destructor style api with a lambda.

Except for the part where destructors are meant to be called no more than once per object, at the end of its lifetime. All that you can guarantee is that `with_file` doesn't call the destructor more than once. But that's not terribly interesting.

“Throw an exception on explicit use after free” is “memory safe” in exactly the same sense “throw an exception on explicit use of an operation on an argument of the wrong type” is “type safe”. In other words, not at all.

> In Modula-3 or D, as as possible examples, a solution might be destructors or scope attributes.

These still allow you to mismanage resources.

> The only way to actually be 100% safe would be if everyone would be programming with formal logic,

Indeed. In order to construct a correct program, you also need to construct the logical argument that establishes its correctness. So, yes, you have to use formal logic.

> which still requires a lot of research to make it approachable by the average developer.

s/research/education/

You raise the craftsman to the level the craft requires, not lower the craft to the level of an apprentice.

> At least in some languages this is not an issue if one is able to use higher order functions, with bonus points if they allow for trailing lambdas.

I am afraid you are talking nonsense. Higher-order functions make verification harder, not easier, because they hide the point at which control flow is transferred from one module to another. This is backwards, because this point should be prominent, in big neon letters, precisely so that you can tell exactly when a resource stops being available, or when an invariant goes from being “your responsibility” to “someone else's problem”.

> Replying here since your other comment may be gone.

I deleted it because zenhack's reply was better.

> Those are arguably more important if one wants mass adoption with all the library and funding benefits that come with it.

I couldn't care less about “mass adoption”. Also, working on the Right Thing (tm) doesn't require a lot of money. It requires an intrinsic scientific motivation, and patience to polish programs until they are flawless.

> I tell language authors to ignore performance or ecosystem compatibility at their language's peril.

Performance is important, but only after correctness has been established. It doesn't matter how fast a program is if it doesn't work.

As for “ecosystems”, again I couldn't care less.

> Which is actually available in quite a few GC enabled languages.

In existing implementations, not with Rust's static safety guarantees about dynamically allocated resources, sorry. “Just provide some way to disable the garbage collector” raises some obvious (at least to me) questions that are nevertheless not addressed by the alternatives you usually propose:

(0) When does it make sense to disable the GC?

(1) How do we know we are using resources correctly by ourselves?

(2) How do we know we are cleaning up resources correctly by ourselves?

(3) How would you rigorously prove all of the above? (Yes, unlike most other programmers, I do prove my programs correct.)

Tagged records are one possible in-memory representation of sum values, perhaps the most sensible one. But I don't want in-memory representations of sum values. I want sum values themselves.

ML modules are much more than generic packages. ML's module system allows you to take an existing module, hide some of its components, make some of its concrete types abstract, and get a new module. My methodology of enforcing only one invariant in each module is impracticable without ML modules.

As I said before, resource management is first and foremost a matter of correctness, so performance is neither here nor there. While you don't need manual resource management for data structures containing values, you do need it for various types of handles (files, network connections, you name it), which a GC cannot guarantee it will collect at the right moment. There is no reason why you couldn't have GC when it makes sense, and deterministic reclamation where it is required.

Algebraic data types and ML-style modules are non-negotiable.

Because Rust-style resource management is not only about performance, but also about correctness. And the ML crowd cares a lot about the latter - rightly so.

I'd kill for a language with ordinary ML types for values (integers, strings, etc.), and substructural types for objects (file handles, database connections, etc.).

> You pitch "The best automated way to do X!", but in actuality you have a horde of people doing the work initially to figure out the problem before building the actual automation.

It is plain dishonesty.

I fail to see the point of this work. When I program, what I want to see is how each statement relates a precondition to a postcondition. From this point of view, the selling point of value-oriented programming is that conditions are partially reified in the program as abstract types, rather than merely existing in the programmer's head or a separate piece of paper. Note that this does not require the complete absence of mutability: an abstract value may contain the identities of mutable objects, but the role of abstraction is to constrain the ways in which these objects can in fact mutate. Laziness is a prime example of this.

> It's actually rare people need to do proofs. If they do, they can also prove the programs correct with a tool suited for it like Isabelle/HOL or Coq then extract them to the desired language. It's worked for extractions to ML, Haskell, Scheme, and recently C (see below).

It baffles me that people think they can solve the problem of the intractability of systems by piling up more complexity on top.

> There's also been verified LISP's (Scheme48, LISP 1.5) and metaprogramming constructs.

It doesn't make sense to “verify language features”. What you verify is programs. Of course, the Lisp crowd is fundamentally incapable of distinguishing definitions from implementations, which leads to this regrettable sort of mistake.

> So, it could be done in or for a LISP-like language with metaprogramming. I even found two metaprogramming schemes for Coq recently.

This fails to address my original comment. Have you actually understood it? The point was (and still is) this: “Metaprogramming might write half of your program for you, but it won't help one iota with the proof of correctness unless the base language is already something mathematically nice to work with.” The excessively operational definition of pretty much every Lisp dialect in existence makes it prohibitively expensive to formally analyze the humongous swathes of code generated by Lisp macros. The problem with Coq is, surprisingly for something coming from the type theory crowd, exactly the same: You can't really understand a Coq proof script just by reading it. Instead, you have to replay it. Operational thinking does not scale.

> That brings me back to an old idea I was just discussing with someone about SPARK. (...)

This sounds insanely complicated. The only justification I can come up with for this kind of thing is manager thinking: “This process has lots of steps and makes people's lives miseable, hence I must be doing something right!”

> languages with good metaprogramming facilities let the users them to fit their needs.

No amount of metaprogramming can fix the intractability of proving programs correct in the base language, especially if the metaprogramming facilities leak identifiers like a sieve (unhygienic macros).

> userland extensibility can play a huge impact on the overall cleanliness of the language because new ideas can be tried out as libraries.

Instead of (uselessly!) trying new language features, how about trying to find usable proof principles for the language features that you already have?