I want to implement a cubical type theory based proof assistant from scratch. Any pointers for how to get started? There's a good research reason for this
10
6
58
Conversation
williamjbowman.com/#depmacros
Can't help with the cubical part, but we've got some infrastructure for quickly building (dependently) typed languages
1
9
It is going to be in Rust, which I'm sure sounds crazy but there's a reason for it
8
15
You might find this helpful (current project I'm playing with) github.com/pikelet-lang/p
2
2
Random question but do you know a good reference (beyond elaboration zoo) for how to do elaboration of metas in this set up?
2
Separately I think Pikelet sounds super interesting, did you have any particular inspirations on the systems programming/ low-level side of things?
1
I find D, Rust, Sixten, Discus, Forth, Gibbon, Red/System, etc. to be pretty interesting! But I'm rather far off being able to experiment with that kind of thing yet. Just sick of waiting to be able to do low-level programming with dependent types, with a nice user experience!