A Programming Language for Implementation of Logic

In the last few years, I have been trying to implement
logic in C++. Most problems (for example memory management)
can be nicely solved, but in the end, the type system
of C++ is not flexible enough. This results in code 
whose type correctness can be checked only at runtime
(dynamic type checking) or that is completely unsafe
(no type checking at all). 

Initally, I tried to implement a library for tree-like
datastructures, with an own type system. At some
point, I decided to add an interpreter to it.
At this point, one might as well call it a 
programming language.

So, I introduce a new programming language, with a 
flexible type system, that it designed for implementation
of logic. It can be efficiently compiled into C,
and some parts of it have been implemented.

Its main feature is its type system: 
Types can be enhanced with subtypes (called 'adjectives').
The compiler is able to infer adjectives for 
variables and intermediate results by means
of abstract interpretation. 

Adjectives are used for deciding which subfields
of a variable exists. This is important in logic,
where a formula has different structure, dependent
on its main operator.

Adjectives are also used for function-call overload
resolution. This makes it easy to construct logical 
formulas.

The language is still statically type checked,
so that its efficiency can be expected to be comparable
with direct encoding in C.

Syntax is mostly copied from Python.