It feels so weird to program in languages that compile modules not top-down as #Lean4 does.

On one hand, it's really cool that I can now put the most important functions up top; on the other hand, it defies logic!