Moreover, Litex aims for more than simpler syntax, it wants to align formal code semantics to daily math: for example, in lean, 1 / 0 returns 0, (1 : Nat) - 2 returns 0. These are very strange to normal people. Litex tries to eliminate the gap between formal code and "real math".