  Technically speaking, the transcendental syntax is about designing logics
with a computational foundation. It suggests a new framework for proof theory
where logic (proofs, formulas, truth, ...) is no more primitive but computation
is. All the logical entities and activities will be presented as
formatting/structuring on a given model of computation which should be as
general, simple and natural as possible. The selected ground for logic in the
transcendental syntax is a model of computation I call "stellar resolution"
which is basically a logic-free reformulation of Robinson's first-order clausal
resolution with a dynamics related to tile systems. An initial goal of the
transcendental syntax is to retrieve linear logic from this new framework. In
particular, this model naturally encodes cut-elimination for proof-structures.
By using an idea of "interactive typing" reminiscent of realisability theory,
it is possible to design formulas/types generalising the connectives of linear
logic. Thanks to interactive typing, we are able to reach a semantic-free space
where correctness criteria are seen as tests (as in unit testing or model
checking) certifying logical correctness, thus allowing an effective use of
logical entities.
