> declared in separate translation units Now if I include both library headers in code that attempts to plug them together, the types will be incompatible. Although not a proof in itself, GCC and Clang seem to agree:…
> Taking the pointer to payload[] field is in no way different from doing "(char*) x + offsetof(struct node, payload)" It may differ, depending on the precise notion of provenance being applicable. If provenance only…
> how does this work? Like this: struct thread { // Entry in the list of threads of the containing process list_node process_entry; // Entry in this thread's scheduling queue list_node sched_entry; // ... }; Each struct…
We mean compatible as defined by the C language standard. It is much more restrictive than having the same layout. In particular, you may not pass a pointer to a type where a pointer to an incompatible type is expected,…
[delayed]
> IIRC GCC and Clang lets character types alias to any type. It is always legal to access the memory representation of any object as an array of characters. The other way around (interpreting an array of characters as a…
> as long as the struct tags are the same Exactly. Now you have a naming problem. You need a naming convention that every user of the list library must follow, or else their types will be incompatible. And what about…
> There is no OoB access of an array Yes, there is. It does not matter that storage happens to be allocated beyond the end of said array. Strict aliasing implies that it is UB to reinterpret the array as anything else.…
> I do not think a type-safe macro-generated list in C is any more awkward to implement or inferior to a C++ template version. I have some experience with this, and while this is one of these things that are feasible, I…
Zero-sized arrays are not standard. Accessing an array out of bounds is UB. At the very least, you should use a flexible array member instead (char payload[];). But even if you did that, strict aliasing implies that…
The go a bit further than the article on the advantages of intrusive data structures, taking linked lists as an example: As the article mentions, intrusive data structures naturally lead to one fewer indirection. To do…
> a single proof covering the most precise description of the program's behavior is more compact Yes, and a program is most compact when all modules have been merged, and all functions with a single caller inlined. We…
In my view, a major selling point of dependent types when it comes to reasoning, is that by bundling logical properties with a runtime value, they require no separate effort to prove the propagation of the logical…
I am not sure what you mean. Of course proving a new property generally implies reasoning on each elementary step of the program. My point is that, assuming you have already proved a property, proving a new one…
I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent…
> probably meaning on an address that’s a multiple of sizeof(int), but who knows Sigh. s/sizeof(int)/_Alignof(int)/. There are good reasons for an implementation to have sizeof(int) = _Alignof(int) and not a mere…
Type punning via unions is not UB in C in general, but it is in C++ IIRC. I write "in general" because, as with other forms of memory reinterpretation (memcpy or copy through a character type), evaluating a trap…
So there are now two ways to represent the same state: None or Some(struct whose fields are all None). Even though one of these representations is never produced by the deserialization routine, anyone could construct it…
This reminds me of Jacques Carelman's Catalogue d'objets introuvables. Highly recommended. It has already been mentioned on HN: https://news.ycombinator.com/item?id=9789216
Capturing invariants in the type system is a two-edged sword. At one end of the spectrum, the weakest type systems limit the ability of an IDE to do basic maintenance tasks (e.g. refactoring). At the other end of the…
Years ago the research team behind OCaml released Chamelle, a version of the language localized in French, as an April fool's joke: https://gallium.inria.fr/blog/ocaml-5/
I would put the emphasis on a different word: > This article is made and published by Anna Hartz, which may have used AI in the preparation Which, not who. They're not even sure the author is human!
Head and tail make sense for persistent lists in functional languages with value semantics, yes. The intrusive, mutable, doubly-linked loops with reference semantics under discussion are quite different. Although all…
> Are you saying the only real way to program is with generic data structures? Certainly not. As I said, the experienced programmer knows when (not) to use them. Some programs are better off without them, such as...…
> declared in separate translation units Now if I include both library headers in code that attempts to plug them together, the types will be incompatible. Although not a proof in itself, GCC and Clang seem to agree:…
> Taking the pointer to payload[] field is in no way different from doing "(char*) x + offsetof(struct node, payload)" It may differ, depending on the precise notion of provenance being applicable. If provenance only…
> how does this work? Like this: struct thread { // Entry in the list of threads of the containing process list_node process_entry; // Entry in this thread's scheduling queue list_node sched_entry; // ... }; Each struct…
We mean compatible as defined by the C language standard. It is much more restrictive than having the same layout. In particular, you may not pass a pointer to a type where a pointer to an incompatible type is expected,…
[delayed]
> IIRC GCC and Clang lets character types alias to any type. It is always legal to access the memory representation of any object as an array of characters. The other way around (interpreting an array of characters as a…
[delayed]
> as long as the struct tags are the same Exactly. Now you have a naming problem. You need a naming convention that every user of the list library must follow, or else their types will be incompatible. And what about…
> There is no OoB access of an array Yes, there is. It does not matter that storage happens to be allocated beyond the end of said array. Strict aliasing implies that it is UB to reinterpret the array as anything else.…
> I do not think a type-safe macro-generated list in C is any more awkward to implement or inferior to a C++ template version. I have some experience with this, and while this is one of these things that are feasible, I…
Zero-sized arrays are not standard. Accessing an array out of bounds is UB. At the very least, you should use a flexible array member instead (char payload[];). But even if you did that, strict aliasing implies that…
The go a bit further than the article on the advantages of intrusive data structures, taking linked lists as an example: As the article mentions, intrusive data structures naturally lead to one fewer indirection. To do…
> a single proof covering the most precise description of the program's behavior is more compact Yes, and a program is most compact when all modules have been merged, and all functions with a single caller inlined. We…
In my view, a major selling point of dependent types when it comes to reasoning, is that by bundling logical properties with a runtime value, they require no separate effort to prove the propagation of the logical…
I am not sure what you mean. Of course proving a new property generally implies reasoning on each elementary step of the program. My point is that, assuming you have already proved a property, proving a new one…
I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent…
> probably meaning on an address that’s a multiple of sizeof(int), but who knows Sigh. s/sizeof(int)/_Alignof(int)/. There are good reasons for an implementation to have sizeof(int) = _Alignof(int) and not a mere…
Type punning via unions is not UB in C in general, but it is in C++ IIRC. I write "in general" because, as with other forms of memory reinterpretation (memcpy or copy through a character type), evaluating a trap…
So there are now two ways to represent the same state: None or Some(struct whose fields are all None). Even though one of these representations is never produced by the deserialization routine, anyone could construct it…
This reminds me of Jacques Carelman's Catalogue d'objets introuvables. Highly recommended. It has already been mentioned on HN: https://news.ycombinator.com/item?id=9789216
Capturing invariants in the type system is a two-edged sword. At one end of the spectrum, the weakest type systems limit the ability of an IDE to do basic maintenance tasks (e.g. refactoring). At the other end of the…
Years ago the research team behind OCaml released Chamelle, a version of the language localized in French, as an April fool's joke: https://gallium.inria.fr/blog/ocaml-5/
I would put the emphasis on a different word: > This article is made and published by Anna Hartz, which may have used AI in the preparation Which, not who. They're not even sure the author is human!
Head and tail make sense for persistent lists in functional languages with value semantics, yes. The intrusive, mutable, doubly-linked loops with reference semantics under discussion are quite different. Although all…
> Are you saying the only real way to program is with generic data structures? Certainly not. As I said, the experienced programmer knows when (not) to use them. Some programs are better off without them, such as...…