mycroftiv @mycroftiv@computerfairi.es
Software developer seeking cooperative collaborations to make the world a safer and better place for all beings. Special interests: Agda, Plan 9, hypercubic communications networks, interactive fiction, bipolar hypomania as a source of artistic creativity, preserving the good aspects of 20th century psychedelic counterculture while filtering out remants of kyriarchical oppression. Peace and love to all beings, human and otherwise.
Suzette Haden Elgin created the Laadan language with a grammar that includes the source of knowledge in how assertions are stated. This reminds me of how Agda allows the inclusion of proofs about the data within its data structures.
After about ten hours a day of learning Agda during the month of September, I'm starting to feel like I have basic fluency in the concepts and how to express my ideas in code. It's been quite the journey since I typed in 10 PRINT HI 20 GOTO 10 on an Apple ][+ in 1982. Still feels like I'm just getting started.
Software developer seeking cooperative collaborations to make the world a safer and better place for all beings. Special interests: Agda, Plan 9, hypercubic communications networks, interactive fiction, bipolar hypomania as a source of artistic creativity, preserving the good aspects of 20th century psychedelic counterculture while filtering out remants of kyriarchical oppression. Peace and love to all beings, human and otherwise.
