Предусловие над чертой

Type Assignment так бля епта, тут у нас предусловие над чертой и если оно выполняется, то... таааак, падажжи ебана x:T ∈ Γ Γ ⊢ x:T x ∉ FV(U) Γ ⊢ x:T Γ,x:T ⊢ u:U Γ ⊢ let x=t in u:U Γ,x:T ⊢ t:U Γ ⊢ λ(x:T)t:∀(x:T)U Γ ⊢ x:∀(z:S)T Γ ⊢ y:S Γ ⊢ xy:[z:=y]T Γ,x:T ⊢ d:T Γ ⊢ ∀(x:T)d:μ(x:T) Γ ⊢ x:T Γ ⊢ μ(x:T) Γ ⊢ x:T Γ ⊢ x:μ(x:T) Γ ⊢ x:T ∧ U Γ ⊢ x:T Γ ⊢ x<U Γ ⊢ t:U

На слайде с заголовком «Type Assignment» докладчик объясняет правила типизации, эмоционально реагируя на предусловие, обведённое красным. Шутка в том, что сложная формальная логика внезапно подаётся как раздражённая попытка разобраться в условии над чертой; мем отправляют как реакцию на запутанный код, документацию или слишком сложное правило. EN: On a slide titled “Type Assignment,” a presenter explains typing rules while reacting emotionally to a precondition circled in red. The joke is that complicated formal logic is suddenly presented as an exasperated attempt to figure out the condition above the line; people send this as a reaction to confusing code, documentation, or an overly complicated rule.

• @profunctor_io / 3267 2019-10-22