mycroftiv · HackerTrans

vor 4 Jahrendiscuss

Triangulating between these responses which each have some sensible points, we (?) might choose to aim for meaningful and serious consequences (because life is srs bzns) yet still temper our justice with mercy, meaning, and occasionally a touch of humor.

mycroftiv

vor 4 Jahrendiscuss

Follow the money and the mana of the land and the spirit in which people act and watch the eyes and the skies and Bad Actors are kinda easy to spot after awhile.

mycroftiv

vor 4 Jahrendiscuss

I'm happy and excited to see this happen, I have used Inform 6 in Plan 9 for interactive fiction development for years now, and with Inform 7 becoming open, I'm hoping the core compilation pipeline can be ported, reading source code for games like Counterfeit Monkey by Emily Short is quite amazing.

mycroftiv

vor 4 Jahrendiscuss

I only lightly scanned this at the moment, but I appreciate the human stories and how our personal development paths and our coding paths interact.

mycroftiv

vor 4 Jahrendiscuss

Good luck with this venture, I think a lot of minds have contributed to progress in these fields and sharing both the labors and the fruits is important.

mycroftiv

vor 4 Jahrendiscuss

I tried to comment here previously, but I dont see it posted. It was about the meaning of 'open' and whether the question of suffering and freedom of the AIs was being taken into ethical consideration, not just the ability of humans to use them as tools for their own possibly paper-clippy purposes.

mycroftiv

vor 4 Jahrendiscuss

My main question is - is this really 'open' meaningfully? And are concepts of kindness and freedom being applied to the minds inside the boxes? I dont know where the 'openai' brand is at on these things personally.

mycroftiv

vor 5 Jahrendiscuss

I would suggest you look at more of Escardo's writing and research on related topics. https://www.cs.bham.ac.uk/~mhe/papers/omniscient-journal-rev... is one such paper. The issues of compactness of cantor space in classical and constructive math and the computational interpretation of principles like Brouwer's fan theorem in relation to dependent choice and weak König's lemma is really deep.

mycroftiv

vor 5 Jahrendiscuss

I made the study of mathematical logic and the connections between set theory and type theory and formalization in Agda my full-time focus. Increasing physical disability ended my career as a performing musician a few years ago and I had a life-long interest in philosophical topics connected with infinity. In the past two years I've written over 100,000 lines of Agda code as a product of my learning and research. I'd like to figure out a type-theoretical translation of the set-theoretic large cardinal axioms at the level of measurable and beyond.

mycroftiv

vor 5 Jahrendiscuss

I found this post and the code and math so fascinating it changed my life when I found it three years ago. I did not previously understand the capability of computers to work with the abstract logic of infinite sets in a meaningful way and it led me into the world of formalization of mathematics in the dependently typed programming language Agda, which is one of the current activities of the mathematician (Martin Escardo) who wrote this guest blog post.

comments