This is a self-response, but I've thought of a case where it might be fairly difficult for a compiler to prove a variable is always initialized, because of the

This is a self-response, but I've thought of a case where it might be fairly difficult for a compiler to prove a variable is always initialized, because of the use of pointers. Take this function to copy a linked list in C: struct node { struct node *next; int data; }; struct node *copy_list(struct node *list_node) { struct node *new_list, **indirect; indirect = &new_list while (list_node != NULL) { // Pretend malloc can't fail struct node *np = malloc(sizeof(*np)); np->data = list_node->data; *indirect = np; indirect = &np->next; list_node = list_node->next; } *indirect = NULL; return new_list; } The variable "new_list" is always initialized, no matter what, even though it's never explicitly on the left hand side of an assignment. If the while loop never ran, then indirect is pointing to the address of new_list after the loop, and the "*indirect = NULL;" statement sets it to NULL. If the loop did run, then "new_list" is set to the result of a call to malloc. In all cases, the variable is set. But it feels like it would be hard for something that isn't a formal proof assistant to prove this. The equivalent Rust code (unidiomatic as it would be to roll your own linked list code) would require you to set "new_list" to be None before the loop starts.