Engineering with evidence
Follow a program from source through checking and bytecode to execution. Explore the evidence behind the language’s guarantees.
Under the hood
Panackelty brings together a compiler, a runtime and a body of verification work. Here is what those engineering milestones mean—and why they matter.
A compiler translates a program into instructions the runtime can execute. Panackelty’s compiler is itself a Panackelty program: the language is substantial enough to implement its own language tooling.
Why it matters: self-hosting exercises real parsing, data structures, type checking and code generation together, far beyond a collection of demonstration programs.
Explore the compiler source →A checked-in compiler seed starts the build. Successive compiler generations compile the compiler and standard-library conformance program; the bootstrap gate checks that the resulting artifacts match byte for byte.
Why it matters: the project tests a repeatable route from source back to its own toolchain. This is strong consistency evidence, not a mathematical proof that the compiler has no bugs.
Read the bootstrap evidence →Source loading, parsing, name resolution, type and effect checks, bytecode emission, verification and execution form one toolchain. Source programs and saved bytecode both run on the C11 VM.
Why it matters: these parts must agree on the meaning of every operation. Bytecode is checked as untrusted input before execution.
Explore the architecture →Exact numeric representations, checked domain values and explicit purity affect the compiler, bytecode and runtime—not just how code looks. The experimental async slice also coordinates suspension and typed completions across those layers.
Why it matters: useful language guarantees require consistent behaviour through the entire execution path, including error cases.
Inspect the specified behaviour →The project exercises malformed bytecode, allocation failures, runtime traps and cancellation, alongside compiler tests and complete programs. Sanitizers and Linux/macOS packaging checks add evidence beyond successful example output.
Why it matters: resource cleanup, rejection paths and distribution failures are part of building a dependable toolchain. Test coverage measures execution, not an absence of defects.
Read the test evidence → Browse test coverage →Get a concrete explanation for a subtraction proof or a local effect decision, with source locations and explicit limits.
Learn to use panack explain →Keep exploring