Jan Růžička se věnuje teorii typů. Co je teorie typů? Jde o matematický formalismus, který lze použít k popisu počítačových programů. Jeho prostřednictvím lze průkazně dokazovat vlastnosti existujících programů. K čemu je to dobré? Programy musí být spolehlivé – např. systémy v letadle, automobilu či lékařských nástrojích. Opetopy jsou matematické struktury, které se podobají vícedimenzionálním stromům. To se v teorii typů hodí, neboť téměř všechny koncepty, s nimiž pracuje, se řídí stromovou strukturou. Stromovou strukturu si lze představit jako hierarchii komponentů a právě na hierarchiích je založena většina (nejen) počítačové infrastruktury (souborové systémy, běžící aplikace, koordinátory semaforů), opetopy nejsou prvním pokusem o formalizaci programů. Zhruba od 90. let se začalo objevovat mnoho efektivních a robustních programů, které slouží k formalizaci jiných programů. Říká se jim asistenční důkazové systémy. Navzájem se liší svou vnitřní teorií, která udává, jak snadno/rychle lze určitá tvrzení dokázat a jakou „sílu“ daný asistent má (kolik tvrzení je teoreticky schopen dokázat). Společné mají to, že důkazy reprezentují textuálně, a to i přesto, že většina objektů, které počítače využívají, jsou hierarchicky strukturované. Jsou opetopy v tomto ohledu lepší? Ano; důkaz týkající se nějakého programu, zakódovaný v opetopu, často odráží podobu daného programu. Je tedy nejen snazší jej pochopit, navíc se nám otevírají nové možnosti k větší automatizaci či znovupoužití důkazů, založené na strukturní podobnosti dvou programů. Navíc důkazy zapsané v opetopech jsou poměrně kompaktní a triviálně přenositelné. Díky tomu na jednom může snadno pracovat více lidí naráz. Opetopy jsou zatím ve fázi matematického výzkumu. Existuje však několik nástrojů, které umožňují praktickou manipulaci s nimi: jeden vyvinul Jan Růžička v rámci své maturitní práce. K průmyslově použitelnému nástroji ještě zbývá vyřešit několik otázek, ale po technické stránce lze jeho omezenou podobu vytvořit již dnes.