Viewing profile — el_pollo_diablo

> 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 funct…

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 pro…

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…

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-trivia…

> 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…

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 cha…

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 deserializa…

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. r…

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 …

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 discussi…

> 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 …

You mean the downside that we also already know, i.e. that there are some situations where a custom data structure would be superior for various reasons (e.g. smaller footprint)? E…

Absolutely. Wrapping the distinguished entry point in a new structure type equipped with a thin type-safe wrapper API that covers the most common use case is the way to go.

Not to mention that they insist on calling every entry of the list a "list head", which makes no sense (hysterical raisins, maybe?). The structure is made of a uniform loop of entr…

None, but that is not my point. Before C23, fn() already meant the same thing as fn(void) in function definitions , which the situation under discussion here. C23 changed what fn()…

Sure, but it is also very common for C programs to contain data structures that have one use in the program, and could still be instances of a generic type. You mentioned red black…

If, by "situation", you mean the development of a small program with so many constraints that using existing libraries is out if the question, then yes. Otherwise, that seems unwis…

Sure, but your alternative code incorrectly assigns to (list)->payload. You have many other options. Without typeof, you can if(0) the assignment, or check type compatibility with …

This is about a function definition, not a random function declarator. C23 does not change anything in that case.

C23 does not change anything in this situation, because we are talking about the definition of main(), not a forward declaration. More details here: https://news.ycombinator.com/it…

Sure, that sort of language-specific idiosyncrasy must be dealt with in the compiler's front-end. In TFA's C example, consider that their loop while (i just needs a slight transfor…

> In fact, even state-of-art compilers will break language specifications (Clang assumes that all loops without side effects will terminate). I don't doubt that compilers occasiona…

> seL4 is the only microkernel that has a proof of correctness ProvenCore ( https://provenrun.com/provencore/ ) has a proof that covers correctness (memory safety, and more general…