Would a proof that the traveling salesman algorithm can't be encoded on LAL also prove P!=NP? An answer to the traveling salesman (and similar) problems can be easily verified on light lambda-calculi. Also, if I understand correctly, the light lambda-calculi can compute every polinomial-time computable function. That way, if one can prove that the traveling salesman problem can't be encoded on the light lambda-calculi, that would also prove the problem can't be solved in poly-time, which would also prove P!=NP. Is that correct, or am I confusing some concepts?
Yes, in the same sense that if you prove that a specific NP-complete problem can't be reduced to a specific P-hard problem, then you also prove P!=NP. The only issue is that the reduction for which P-hardness hold must be "compatible" with the allowed encodings.

From the information you give in the question, I conclude that LAL is P-time hard. The article Light types for polynomial time computation in lambda calculus by R. Baillot and K. Terui confirms this, by showing that DLAL (dual light affine logic) is a P-complete subset of LAL.



My own experience is that many P-complete problems look attractive and natural. My favorites are linear programming and Horn-satisfiability, but I guess that DLAL (or LAL) look even more attractive to you. But even so they are attractive, using them for resolving N!=NP is probably futile. More than one reduction of specific NP-complete problems to linear programming has been published, but the reductions turned out to exponentially increase the size of the problem.