orangea

Your question is answered fairly comprehensively by the other comments on this page which were posted before yours.

VS Code, for better or for worse, has evolved into something like an operating system or programming language VM, capable of running apps (extensions) which do useful things while only interacting with the VS Code extension API. This allows one to use such "apps" without installing VS Code.

Theoretically, one could run code in vscode.dev if an extension provides a programming language runtime. I'm not sure if there are any extensions which do this yet.

It is interesting to think about how many general-purpose VM-like abstraction layers are sitting on top of each other to run this — the operating system provides an interface which the browser uses, the browser provides an interface which vscode.dev uses, vscode.dev provides an interface which an extension implementing a programming language runtime uses, and the program uses the runtime interface.

Github Codespaces has the downside that you need to connect to a cloud computer and do all your development remotely on the cloud computer, which causes issues such as lag, the need to pay money for the service, inability to use it without an internet connection, etc. This provides the benefits (however small) of a development environment running in the browser without those downsides.

My guesses:

- People who don't own a computer, e.g. university students who only use the school's computers (or K-12 students even), but who still want their editor settings to be automatically saved and used, and who don't want to deal with installing things on the computers they use (or can't install things).

- People who own multiple computers and who don't want to deal with syncing configuration such as installed tools, editor settings, etc.

I have no idea but maybe it would count as aiding and abetting.

"Imminently" reasonable and rational? What does that mean?

> Do you think it's somehow more altruistic to provide subjectively uglier individuals the same wage? Bias based on attractiveness is no worse than bias based on personality or any other trait. Your point is moot anyway, in a capitalistic society people can just choose to visit another business where the staff has the traits they desire.

Your point seems to be that there is no inherent moral good in distributing resources equally among people as opposed to allowing inequality to naturally emerge and/or optimizing for total value across all people. I don't necessarily disagree: it is hard to argue from first principles that each individual should be given the same weight, as opposed to any other arbitrary system like giving each family the same weight, or taking intelligence into account. However, it is also wrong to pretend that there isn't significant precedent in society for assigning each individual equal moral weight — for example, by allowing everyone an equal vote in elections, which has clearly been a useful practice. And I consider it obvious that "Bias based on attractiveness is no worse than bias based on personality or any other trait" isn't something that would be widely agreed upon.

The "selectopia" example is kind of how it already does work, or at least how it used to, in computer programming, where having an impressive Github account can help one get hired. But it has downsides:

- People who want to get hired put low quality projects on their Github which are optimized to look impressive at a first glance.

- People spam popular open source projects with low quality pull requests to buff their Github contribution metrics.

- People who don't have the time to create software for free are put at a disadvantage. Also people who aren't passionate about programming enough to have side projects are at a disadvantage (not necessarily bad).

I also suspect that this phenomenon is what motivates the development of a lot of the "leftpad" or "is-even" type libraries. Which could be interpreted as either good or bad.

This is a popular opinion and there are tons of implementations of WYSIWYG text editors such as Typora and Obsidian that attempt to make their data model simple like Markdown. But they all kind of suck, which shows that making that kind of editor is really hard.

Ruby used to have the $SAFE feature for sandboxing, but it was removed because it was buggy, added a lot of complexity, and wasn't actually that useful. Linux has all the various isolation features that make Docker work, but people still recommend not running untrusted code in Docker containers because of the potential for oversights/"bugs" in Linux's API. I suspect that programming languages / VMs don't include these features because they are very hard to get right and add a disproportionate amount of complexity for their utility.

Why are you capitalizing "category theory" and not "topology", "algebra", or "math"?

It is used in some formalizations of quantum field theory. Quantum field theory is used to make testable predictions about physics, and historically, giving scientific theories a rigorous mathematical backing has been useful. So that could be an example.

I meant why not make a project like this that emulates the FUSE API, but use the file provider API to present the file system to the OS instead of NFS. It would have the advantage that it would be better integrated with the OS, for example you can display upload progress indicators on files in Finder. Maybe that can also be done with NFS though, I don't know.

Why not use the file provider API? https://developer.apple.com/documentation/fileprovider

What is this "shove" operation and how is it different than moving a file the normal way?

society had those values, it doesn't mean that society embodied those values.

The only way to understand math like that is to do the hard work of learning by reading textbooks and other learning materials and doing exercises. Comments sections won't help you for learning this kind of advanced math.

If HoTT is what you are interested in, I recommend this single-page introduction if you are already familiar with how dependent type theory is used for theorem proving: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes...

It is my understanding that HITs are just as easy to integrate into non-homotopy type theories as they are to HoTTs.

Which has nothing substantial to do with category theory.

How can homotopy type theory, as opposed to non-homotopy type theory, help us with "verification of systems/hardware and formalization of math" outside of homotopy theory itself?

My perspective has always been that it can't.

I don't mean any offense to you personally, but this kind of comment is why I hate internet discussions. You just said the opposite of what I said without adding anything new.

That's not a reason, that's a definition.

Why more useful than non-homotopy type theory?

One thing that has always bothered me is how people say that ideas from category theory can be useful while writing Haskell code. It's technically true, but really only the most basic ideas — things which would be in the first chapter of a textbook on category theory, and which many might not even consider to be part of category theory itself. (For example, every type in Haskell is inhabited, which alone somewhat limits what you can say about it...)

And then there is also the fact that there is a huge difference between the skills and ideas that are useful for writing proofs in a theorem prover and those that are useful for writing quality software.

Also, anything having to do with homotopy type theory is even further removed from programming than regular type theory. Correct me if I'm wrong but I think that it is really only useful for helping prove theorems in homotopy theory, rather than being more generally useful for other kinds of math.

Why does HN seem to be so much more interested in homotopy theory and related fields than other fields of math? I'm not a mathematician, and my understanding is that this "area" (including algebraic geometry, algebraic topology, and related areas of mathematical logic) represents a very small proportion of what career mathematicians actually work on. Does HN just like this subject because it is trendy? Because of its reputation for being difficult? Because of perceived connections to programming (of which I believe are generally exaggerated)?

Everything after the first 1-2 paragraphs in the readme is in English.

There are a lot of features which a markdown editor can have which are somewhat difficult to implement and get right, such as WYSIWYG with css theming, support for latex equations, support for nonstandard features like Pandoc markdown, plugins, support for the textbundle format... Nothing exists that implement these perfectly and so I think people make attempts at making something that at least works for their specific use case but no one can make the one true editor that does everything because it would be a huge amount of work.

Is it still in beta?

I wonder if services like gitpod/github codespaces/repl.it would be a good solution for allowing people to use an agda environment without installing it.

Does the "fundamental group of the circle" part use anything specifically from homotopy type theory as opposed to any other type theory?

Unfortunately this doesn't seem to be actively being worked on and isn't complete enough for me to use personally (custom themes aren't implemented, for example).

These are the WYSIWYG Markdown editors that I am aware of:

- Typora (great but somewhat buggy).

- Obsidian is working on a WYSIWYG mode.

- Nota (nota.md) is promising but very beta.

- Zettlr

- Bear is working on a WYSIWYG mode.