Show HN: Εἶδος – A non-Turing-complete language built on Plato's Theory of Forms
proletarian Wednesday, February 11, 2026I've been reading Plato text and picking up some ancient Greek, and I had a useless thought experiment: what would a programming language look like with 4th century Athens constraints?
Εἶδος (Eidos — "Form") is one result. It's a declarative language called Λόγος where you don't execute code — you declare what exists. Forms belong to Kinds. Forms bear testimony. A law of correspondence maps petitions to answers. There are no loops, no conditionals, no mutation. It's intentionally not Turing-complete, aligned with Plato's rejection of the apeiron (the infinite).
It governs a real HTTP server (Ἱστός) where routes aren't matched by branching — they're recognized as Forms and answered according to law. An unrecognized path returns οὐκ ἔστιν ("it is not") — not an error, an ontological statement.
The project includes a parser that recognizes rather than executes, static verification expressed as philosophical propositions (Totality, Consistency, Well-formedness), Graphviz ontology diagrams, and a Socratic dialectic generator that examines the specification through the four phases of the elenchus.
The Jupyter notebook walks through everything interactively — from parsing the spec in polytonic Greek to petitioning the live server to watching Socrates interrogate the ontology.
https://github.com/realadeel/eidos