Inspired by this:
This is a level pack containing intentionally impossible Baba Is You levels.
Now I'll bet there's probably some brute-force method for this that considers every possible move. But is there some algorithm to determine the possibility of a Baba Is You level?
Building on @quazmlpok's answer, and the comments on that answer:
Given sufficiently large (but not infinite) memory, you can make an algorithm that solves the halting problem for any Turing machine that itself has bounded memory. the trivial solution is to simply enumerate all possible states of the memory (here, all different combinations of all the possible blocks), and run the game for one step times 5 for each of the actions you may perform. For each state, either it terminates (winning, dying, crashing, hard-crashing) or it transforms into another state that you by definition also solved. You can then build a graph of all states and identify which ones are part of a loop (never halts) and which ones are part of a chain that ends up halting.
I could not find an estimate for the total number of different blocks that may (or may not) be placed in a level, but it seems there are more than 100 Property blocks alone. Taking the worst-case scenario of 2048*2048-size levels, and assuming a reasonable 1 byte per square, you would need 2048^2^100^5 bytes, a number with 3312 digits. This is only for properties but the maths holds for larger finite numbers of different placeable things.
For context, this is A LOT more than there are atoms in the universe (I am struggling to express how much "number of atoms in Trillions of universes" does not even make a dent in that number), but from a pure maths standpoint, this very far from infinity. If you could somehow build a computer to store all these level states, then you could solve the halting problem for BIY.
This all assumes that BIY is deterministic (it is not: e.g. the Chill property, though you could also enumerate all possible resulting states from the random movements, since that is also a countable number), and it also doesn't take into account the fact that more than 1 thing may be occupying a square (through stacking).
I'm actually unsure on how to approach stacking, because it creates additional states that you cannot enumerate by simply placing something on squares, and as far as I know stacking can be infinite. if stacking can be infinite (disregarding Too Complex! and the like), then the game is probably truly Turing complete and its halting problem is undecidable. If stacking has a limit i'm not aware of, then the number of states would grow even more extremely large, but it would still be possible to enumerate all possible stacks on all possible squares, and solve the halting problem.
This is across all possible levels, therefore for a given level (that does not permit stacking, for simplicity), you can simply find the starting state of the level in the graph, and find a path of moves that gets it to win, or you don't and the level is impossible.
Baba is You is Turing complete, as demonstrated in this twitter post that implements Rule 110.
In practice this will run up against the 33x18 maximum level size, but according to reddit it's possible to use debug mode to get at least 2048x2048.
I'm not well versed enough in computer science to put this into any kind of real proof, but I believe the result of this is that knowing for certain if a level has a success state is equivalent to the halting problem, and therefore it is impossible.
I imagine it's also possible to do something similar to the passcode Mario Maker levels, where there is a solution but it's functionally impossible for another user to solve because they don't have the key.
