mycroftiv

no profile record

comments

4 ปีที่แล้วdiscuss

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.

4 ปีที่แล้วdiscuss

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.

4 ปีที่แล้วdiscuss

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.

4 ปีที่แล้วdiscuss

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.

4 ปีที่แล้วdiscuss

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.

4 ปีที่แล้วdiscuss

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.

4 ปีที่แล้วdiscuss

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.

5 ปีที่แล้วdiscuss

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.

5 ปีที่แล้วdiscuss

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.

5 ปีที่แล้วdiscuss

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.

6 ปีที่แล้วdiscuss

Thank you, I remember your participation back in that era. The main useful thing that emerged somewhat recently is the system called 'spawngrid' which leverages fossil rootscores, venti replication, and independent namespaces provided by ANTS to spawn independent plan 9 environments on demand and make them available on multiple nodes. It was a bit too ambitious for the real world so I'm going to stop wasting the money on running the unused servers but it did work pretty well in the technical sense. The lighter and simpler public grid will continue because it has an active user community.

I also developed a lot of interest in more theoretical computing topics which I may or may not be able to bring toward Plan 9 namespaces at some point, but I don't have the time to summarize that here, the blog on my site covers some of the ideas.

6 ปีที่แล้วdiscuss

I've done some experimental setups using hypercubic routing and algorithms inspired by 80s supercomputer designs from the nCUBE corporation, and the 'spawngrid' is a lighter-weight plan 9 take on containerized service architecture, so I'd say the answer is yes.

6 ปีที่แล้วdiscuss

From the discussions I've had over the years with the primary 9front maintainer, the balance of adding new features and complexity and the fact that ANTS is most effective in combination with the Fossil file server which base 9front removed from its distribution means that it goes in a different direction than 9front's goals. Some software which is part of ANTS such as 'hubfs' (9p muxfile/message queue) may be integrated into 9front via a different author's rewrite as 'mq' and some other ideas from ANTS may eventually result in 9front code and changes, but the ANTS patchset for 9front was around for several years and didn't attract enough users to create any groundswell of demand for integration into the base.

6 ปีที่แล้วdiscuss

It's mostly hobbyist Plan 9 software development. There is some shared disk storage and people upload code they are working on for other people to test and help with, so it is an active workspace for Plan 9 development. There is also a lot of general discussion of computer related topics in the chat, sometimes with a rather abstract mathematical focus on limits of computation and dependent type theories and the logic of infinity, with only a vague connection to existing Plan 9 software - far out brainstorming.

6 ปีที่แล้วdiscuss

No, its not wise from a security perspective, the grid operates in a very fragile zone of 'nobody except a small number of plan 9 users knows or cares about this and there is no incentive for malicious behavior' - we have been very lucky in that it seems that using Plan 9 and taking the time to learn how to connect to the grid seems to filter out people who just want to be destructive or malicious. At some point it may prove to be a problem but we have gotten along ok for a few years. Users also have the choice of what services they use and some users dont use the plumber for auto-sharing in this way.

6 ปีที่แล้วdiscuss

It's about two things mainly: updating the design of the distributed architecture of Plan 9 to be less centralized, and using Plan 9 for ad-hoc resource sharing and communication for hobbyists. These things overlap because I provide grid resources for people to use which run on ANTS-powered servers/architecture.

6 ปีที่แล้วdiscuss

If anyone is curious about what this is all about, feel free to ask, this is my project which has been ongoing in one form or another since 2008.