[LudwigNagasena]

> I feel like no serious work with this ambition

What ambition? The book is an applied introduction for people who aren’t even familiar with what ∃ means. It’s 200 pages, which is at best comparable to a semester-long course.

[js8]

Ambition to help programmers understand logic and how it relates to their discipline. But maybe you're right, it cannot be (currently) done in 200 pages, although I hope somebody proves that wrong.

It kinda reminds me of the debate whether functional programming is suitable for beginners, despite being simpler than imperative, while imperative is more familiar.

I am opposed to familiarity argument (I think classical predicate logic and existential quantifier are being taught in early high school, maybe sooner, so they are more familiar than lambda calculus).

Based on my own programming and math experience, I wish I learnt about functional programming, LC, dependent types and CHI much sooner. I don't think it has to be complicated, I know some attempts (although a bit incomplete) to show this to beginners - To Mock a Mockingbird, Haskell Programming from First Principles.

[LudwigNagasena]

I don't see much value in knowing that dependent types can be used to encode logical quantifiers or similar stuff in applied programming. Maybe there is actual value that it creates after you grok those concepts (beyond the general applicability of any concept or metaphor in your thinking), but I don't see it.

"Functional programming" in applied programming usually just means using less mutable state and using stuff like `map` and `reduce` to make semantics of code more predictable and move the burden of optimizing actual implicit mess it creates to compiler/interpreter.