Nix being an expression based functional language, it doesn’t really make sense to have something like let x=y; since this looks to most people like a statement (i.e. a line of code that gets executed as part of a sequence). This doesn’t exist in nix—instead you have expressions that get lazily evaluated, possibly out of order compared to what you’d expect. let x=y in makes it more clear that the variable binding you’re doing is only in scope for the current expression, which reads something like “let x refer to y in x + 3”
The function definition syntax is unusual but definitely not unintuitive imo. It captures the simplicity of the function semantics of nix—a function is just a mapping/transformation from one value (or set of values) to another. I don’t think it’s too much overhead to learn that they use : to mean this instead of =>
In terms of why they picked this syntax, it follows the traditions of other functional languages such as the ML family, Haskell etc.
Just noticed in euclidean geometry, for any two line segments touching at a point there is exactly one triangle you can draw, i.e. a triangle is uniquely described by any two of its legs. In spherical geometry, there are two choices for the third leg!