[johncolanduoni]

I think the OOP vs FP debate misses the real asset that functional programming offers us, and it's not writing everything in [your favorite functional language]'s typical style. Look at a language like Idris; a formal definition of its unsugared semantics would fit on half a page easily. However it still manages to give us all kinds of goodies, like effect tracking, compile-time checking for virtually any condition you can write a decision procedure for, and design-by-contract on steroids.

These features are useful whether the code you're writing is pure, stateful, object-oriented, functional, and/or whatever paradigm you write up tomorrow. Forget aesthetic arguments about elegance; where else can you build so much without ad-hoc concessions to individual language features? As far as I know, there's no other method that lets you treat powerful language features as libraries without either (a) making a mish-mash when they're used together like compiler plugins do (b) making debugging your compile process a full time job like various strongly-typed macro systems tend to.

Why not use FP to form the fundamentals of our languages, something where as of yet it has no equal, and build up the structures we need (regardless of programming tradition of origin) on top of that?

[svanderbleek]

I like your points, but I'm not sure of the Idris on half a page. How much tacit knowledge does that rely on? We do need to focus on the fundamentals of education, the spectrum of logics with quantifiers, lambda calculus, and natural deduction style presentations of language semantics (not sure what to actually call this?).

[johncolanduoni]

I'm referring to the operational semantics[1]. This doesn't require any tacit knowledge to fix the language past what the horizontal line and definitional equality symbols mean (it's entirely in the form of purely syntactic "given this, you can write this"), but it won't be remotely helpful to teach you what the syntax reductions mean or how to use them. If you're never heard of lambdas, you could technically still "use" them in the sense a computer can, but good luck figuring out that they represent functions. It wouldn't fit any sensible definition of "understanding".

My point isn't that these things are easy to learn because their presentations are so brief; personally, dependent typing took me a long time for me to wrap my head around. What I think the briefness of the operational semantics in combination with the examples of things people have built within them suggest is that they're very versatile. Even if only people working on language level features bother to learn them, the utility of their creations (all without needing to move to another language or introduce possibly incompatible extensions) is a huge asset.

[1]: https://en.wikipedia.org/wiki/Operational_semantics

[delish]

> How much tacit knowledge does that rely on?

It looks like you're criticizing the GP's praise of Idris' concise formal definition of its unsugared semantics. I wouldn't use such a formal definition for educating novices (like I think you're implying in your next sentence); I'd use it professionally to show that many desirable things--effect tracking, compile-time checking, and design-by-contract--derive from the same thing. Ken Iverson in his notes on mathematical notation says that one criterion for a good notation is "suggestibility"--the notation should suggest that other problems similar to those you found just now could be solved as well.

Whether formality is useful for novices, it is certainly useful for experts.

[svanderbleek]

I was just trying to tease out what you need to know so that Idris fits in half a page. I'd actually like to know those things!