> Anyone have any thoughts on an idea I've been pondering for a while: Prolog as a type system [...] traditional formal logic syntax, with resulting usability i

> Anyone have any thoughts on an idea I've been pondering for a while: Prolog as a type system [...] traditional formal logic syntax, with resulting usability issues You haven't really explained what your idea is or how Prolog differs from "traditional formal logic syntax". If anything, Prolog's predicate syntax is closer to formal logic than the many ML-based dependently typed programming languages; except that quantifiers are implicit in Prolog. Anyway, you might want to look around http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/ http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/ and espectially http://www.lix.polytechnique.fr/~dale/lProlog/ http://www.lix.polytechnique.fr/~dale/lProlog/ > requently a mismatch with the programming language I find Coq's syntax fairly regular in this regard. (The syntax for expressing computations and predicates, not the tactic and tactical syntaxes.) > So, why not use a programming language for type-level programming? Because of the "mismatch with the programming language" that you yourself have identified as a problem.