[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!