sdleffler/tarpit-rs

A type-level implementation of Smallfuck in Rust, doubling as a Turing-completeness proof for Rust's type system.

tarpit-rs: Smallfuck implemented in Rust's type system

I wrote a blog post on this! You can find it here.

This is a proof of the Turing-completeness of Rust's type system; it's an implementation of Smallfuck, a known Turing complete language. Since Rust's type system may have a Turing-complete language embedded in it, we know therefore it must be Turing-complete itself! Neat.

Contained in this repository are both the type-level implementation and a minimal, unoptimized runtime implementation for verifying the type-level implementation. Additional tests can be added via the sf_test!{} macro, and run using cargo test.