徐志赫 서지혁

Ivory Cadet: Haskell meets LISP

14 Jan 2017

Orignially posted on Deskthority:

My first topic on Deskthority. Greetings! :)

Ivory Cadet, on my desk at home.

On my way back from work yesterday, I picked up a certain package from Germany at the local post office, ordered nearly a year ago. These long-awaited keycaps were the missing piece to the completion my custom keyboard project, so now I’m happy to share how it all finally turned out!

Cadet is a keyboard controller for the ATmega32u4 written in Ivory, a Haskell EDSL for safe systems programming. Ivory was designed for implementing high-assurance software for UAVs, but why not put it in a keyboard? Space Cadet was a keyboard used on LISP machine, and in this incarnation, its keycaps go on a board with the controller written in Ivory. Hence my keyboard’s name: Ivory Cadet. My academic interest is in software verification and provable correctness, so the logic symbols of the Space Cadet keycaps and the controller implementation language turned out to be a perfect match for me! :D

The switches were actually a gift from cookie, from when I was translating between Happy for running the HHKB metal sticker GB. Thanks cookie! The keycaps are unmistakably the Space Cadet set from 7bit’s Round 6, with small cadet legends. Thanks to 7bit for accommodating my last minute order changes, and of course running the group buy! I couldn’t have finished this board without Deskthority, so thank you all. ;)

What next? Cadet still contains some C code, mostly from the Teensy USB stack. I plan to rewrite these into Ivory. Unicode input support for the logic symbols is a priority too. I’ll make sure to update progress on this thread. I’d also like to see some more ducks on the board and maybe a hashbang, so I’ve put in orders for facetsesame’s Honey Spherical Extras. Lastly, how do I go about bribing 7bit into running the Space Cadet set with front printed legends for Round 8? :evilgeek: