Isn't this solved perfectly with an affine or linear type-aware optimizing compiler? Where all data is immutable unless the types prove to the compiler that there are no mutation conflicts. I believe Rust implements this and Idris 2 does so as well with quantitative type theory.
Interesting point. Lambda calc is equivalent, where the expression can be seen as equivalent to the ticker tape. So when a reduction occurs in lambda calculus, it's just like a group of symbols being interpreted and overwritten. But the thing is, no one has to overwrite the symbols to "reduce" them. It's just a space (memory) optimization. Usually to calculate something (you're fully correct by the way) we do overwrite symbols. The point of using immutable style is simply to make sure that references don't become overwritten. It sucks to have x+2=8 and x+2=-35.4 within the same scope, right? Especially when the code that overwrote x was in a separate file in an edge case condition you didn't consider.
Yes, I mistyped that bit. I meant to say that because types (as a grammar) are values, they can be inputs and outputs of functions. The functions can fill in the hole that dependent/refinement types fill, by taking context into account (the grammars which describe simple types being context free).
Type -> Type fill in for type constructors like this infinite list:
InfiniteListOf = Type ->
Type & InfiniteListOf Type
That function just morphs a simple grammar into another grammar. Imagine now if we could calculate something in between:
IncrementingInfiniteListFrom = number ->
number & IncrementingInfiniteListFrom number+1
That's where the dependent types come in, naturally.
I'm feeling both really pissed and validated right now. I thought this was going to just be a normal thoughtless config language that would only be successful as a Google project. Then I looked at the theoretical basis page. I have no formal proof about this, but I've been talking about this type of a type system with my parents and high school CS teacher for a while now!
My idea sounds like this: a value is simply an actual binary string. The "type" that classifies any data is described as a formal grammar, where the binary string is a formal language. If the language can parse a given binary value with the formal grammar, that value is an element of the set (type). This naturally leads to a structural type system which can be described using existing set theory and implemented using existing parsers and formal language theory. Of course, this leads to type -> type functions which describe dependent and refinement types naturally.
It's great to see this idea being broadcast on the front page here, as I can see it very clearly as a superior type system. I'm really regretting not writing a formal article about it sooner!
I'm on my phone in the country side with slow internet so I cant look up a link, but if I remember correctly, you should search "Alan Savory TED Talk" on youtube for an introduction to the use of livestock to reclaim land. Essentially, the issue with most livestock grazing is that it does not mimic natural grazing, which is a seasonal, high volume, high density event where the herd moves on and allows the grazed area time to recover.
While it is only a design concept, Mercury OS [1] might interest you. When I first came across it, I was blown away by the idea. It basically makes the user intent first class rather than the application/program. What I mean is that instead of finding a program or application to execute your intention indirectly, you declare your intent to the OS. Then the OS maps your intent to a series of actions which are executed by hooked-in pseudo-functions. It erases the boundary between applications by being almost like an interactive visual version of a declarative programming language. You should read the article rather than trouble yourself with my explanation though...
Every once in a while I find a site like yours that has conveniently aggregated a ton of stray thoughts and expands my world a little bit. Just wanted to take a moment to say thanks for doing this
Environmental problems will only be solved if
1) people can earn money by solving it
2) people hit a breaking point, and actually drop what they're doing to help
...and #2 doesn't seem very likely for a while. So the only practical thing to do right now is spread awareness and to support companies implementing #1. I made a comment here about permaculture which I recommend you see [1]. And I also have an example company implementing #1 [2]. And here's an example of #1 actually happening [3].
Exactly. The definition of life that is taught in school and widely cited is very limited to simply what we traditionally consider alive. But where are fr he lines drawn? Must life be conscious, or at least experience qualia? Does conciousness get more "real" in more complex organisms? (Is a fly just as alive as a horse is?) Why do we consider viruses to be not alive? Are our own bodies' cells alive? In what way? The system is very complicated and we answer is with a hand-waving simple definition.
Piping program output is just function composition. The downside is that it works over expensive system processes, and data must be serialized. It's a fragile system where instead of using built-in functions, we use "standard" executables.
That misses my poorly written point. Do you use a separate, awkward tool to call functions you wrote in python? Or do you call the function in python itself?
The shell is a useless abstraction that was only necessary in unix because the alternative was c. Now that we have better languages, why not use them to write the OS bottom-up?
Why did we keep the language of the shell and the OS separate? It seems like a needless abstraction which creates more harm than good (read a shell script vs any other language). While I'm at it, why is the filesystem and syscall api not just part of a standard userland language? For example, the filesystem could be exposed like an object tree rather than some syscall ritual. The syscalls could just be invisible, where the language compiler deals with it instead of the programmer. I think that the old LISP machines got this right while we are stuck in a usless POSIX compatibility trap. The only reason I think they didn't design unix this way was because C was too low level, but we could write the OS in a "higher level" functional language.
"Invent" comes from Latin and simply means "find". If you think about it, no matter what language, there is no fine line. An invention is just a discovery, but we typically use the word to describe a very specific discovery.
Yes, I realize that it is obviously Chinese propaganda, but I used it to show that deserts are entirely reversible. You are right that the altitude definitely has a cooling effect, but it also doesn't change the fact that the trees stabilized a desert into a forest.
This dynamic could change if previously arid land can be put to agricultural or residential use. But that requires a lot of initial investment. The first step I think is to convince people that the problem can be fixed - and be profitable at the same time.
This is extremely obvious and it's surprising how long it took for this to be noticed. If you clear a section of a forest, the area becomes as hot as a desert because of the lack of shade. This is a "microclimate". The more area you clear, the larger this hot microclimate becomes. This is the reason why there is desertification all over the globe.
Whether you believe it or not, it is just as easy to create a desert from a forest as it is to do the reverse [1], it can even be a passive process [2]. Deserts rain occasionally, and when they do, it becomes a flash flood. If you tame the flash flood [3][5], you can change deserts. There are projects that do this and have proven its effectiveness, while also being able to solve the water crisis in arid lands in Africa [6].
Trees are incredibly important not necessarily for their reduction of carbon dioxide, but because of the microclimate each tree creates. They filter harsh light for the undergrowth, they cool the general area, and they transpire around 99% of the water they get, leading to more clouds and then more precipitation in other areas [4].
The reason why projects like this aren't so popular and aren't subsidized is not because they aren't effective, but because it is hard to make money from actually saving the environment.
When a nuke comes to destroy a big developed part of Hawai'i, there's a lot of stuff on the island you might want to get out of there. Maybe, systems are designed to rapidly move that stuff to safety, as soon as an alert triggers it. A Bulk Data Transfer of all sensitive, unique data would probably be hardcoded to start on this emergency alarm. How long would such a BDT take? Maybe somewhere around 38 minutes? Forget data transfers, what else might need to be moved out, that would take more than 30 minutes? This whole situation sounds silly, but what explanation sounds more probable?
Look into DASH, it has a fundamentally different architecture than bitcoin. The biggest pros are instantSend, privateSend, and the DAO (A governance system).
I see you have to respond to everyone in the comments when they call out that this isn't actually native. It is true, and normally, Electron would imply _significant_ performance issues. But, considering this whole thing is a network I/O visualizer, making a truly native app would not help at all in the long run. Also, you get the benefit of a common cross-OS experience. You made the right decision.
I'm making something related as a side project too, and the major problem I have right now is showing a terminal on the page. As you can see I'm relying on archaic methods... https://term.surge.sh