search

AtticusKuhn / parallel-algorithms

Proving the correctness and performance of certain parallel algorithms
4 stars 0 forks source link

Cubical #3

Closed AtticusKuhn closed 1 year ago

AtticusKuhn commented 1 year ago

I am experimenting with the idea of higher inductive types to make sure that all laws and identities are being followed, and to make it only possible to write correct code

AtticusKuhn commented 1 year ago

PR closed because Conal Elliott does not like inductive data types

conal commented 1 year ago

Conal Elliott does not like inductive data types

I do like them for some purposes. As a fundamental specification, they’re the opposite of what I’m after in that they’re all syntax (“free”) and no semantics.