Divine Intellect Compiler

• 

  Users can denote holes using ?

• 

  Here, divinity has filled the hole, and verified the answer.

• 

  This is the big diagram of how the compiler works and typechecks.

• 

  This proof fails, as 4 / 3 isn't two.

• 

  This is corrected, and therefore holds!

Divine Intellect - Very, very good thinking/God-like thinking and reasoning skills

Inspiration

LLMs are great at writing code, but usually offer little in the way of assurance. The Divine Intellect Compiler implements the Divinity language - a verified, dependently typed, toy language with holes. Designed with inbuilt LLM support for filling program holes, then proving these are as intended - run programs directly or build them to SMTLIB2 proofs for more assurance.

• Dependent types allow for more precise control over what a value can contain, for example we can define a BoundedInt, where the value must always be between 0 and 10.

What it does

• Programs can include "holes," placeholders for incomplete parts of the code, these can be filled using an LLM inbuilt to the custom IDE.
• Users can define dependent, refinement types to enforce constraints on what can be held by certain variables.
• The Divine Intellect Compiler will prove the LLMs solution to these holes against the surrounding dependent types, giving developers assurances that what the LLM has done is correct.
• If the LLM writes something invalid, the compiler is able to converse back as to what is incorrect, using information integral to why the proposed solution is invalid.
• The program can either be interpreted directly, or have it's satisfiability proof compiled to SMTLIB2.

How we built it

From the get go, our goal was to develop the compiler in safe Rust. However, by the time midnight rolled around, we decided to transition to a Python interface after grappling with Rust's unreliable Z3 bindings. While the majority of the compiler and interpreter was implemented in Rust, we chose Python for the type-checker and IDE.

Challenges we ran into

In addition to transforming type checking into a satisfiability problem, the Rust bindings for Z3 are good for more optimisation based tasks, but bad for working with more complex data structures such as an AST. It's easier to list these,

• Calculating and encoding type arithmetic in Z3 dynamically was challenging, we use a recursive approach on the AST to generate the constraint, then invert it at the top level to get the 'inverse' of the type.
• Implementing the Parser and Interpreter was difficult, particularly learning the Larlpop format for defining production-rules.
• SSA transform!
• Just in general translating type checking into a satisfiability problem was difficult.

What's next for Divine Intellect Compiler

Ideally we'd like to add list and string support to Divinity - this really unlocks the power of dependent types more but was out of scope for this Hackathon. Dependent types are great for lists because they allow you to encode precise properties, like the length or contents of a list, directly into its type, enabling stronger compile-time guarantees about accessors.

All in all, we're proud to say that we wrote a 1300 line divine intellect compiler.

Oh, and here's an example code snippet if you're REALLY interested in the syntax.

type bankbalance(a: i32) where {
    a >= 0,
};

fn add_to_balance(bal: bankbalance, amount: bankbalance) -> bankbalance {
    return(bal + amount)
};

fn double_balance(bal: bankbalance) -> bankbalance {
    return(bal * 2)
};

fn main() -> i32 {
    a: bankbalance;
    a := 100 - 50;
    return(a)
};

Built With

• python
• rust
• tkinter
• z3-theoremprover