> aimed at programmers rather than mathematicians and computer scientists Do it! There's a dearth of such a format for the more "hi-falutin" topics out there.

> aimed at programmers rather than mathematicians and computer scientists Do it! There's a dearth of such a format for the more "hi-falutin" topics out there. Doesn't need polish or total precision either, "us programmers" can deal with IRC-like stream-of-tid-bits. Question: if compile-time evaluation of language X is fully-featured-fully-capable X (sans IO / syscalls, say) with "types as values" (of compile-time-only type `type`, say), ie. given Turing-completeness, where you can have functions that build up and return types --- do you still need complex theoretical type system constructs like "dependent"/"refinement"/"row-polymorphic" etc natively.. say at compile time, given sufficient prim builtins and storage-describing "prim types" (int, arr, tup) any further type-details are described programmatically. I suppose this leads to being able to express predicates that the type checker can "evaluate" in tandem with those compile-time evals..