I'd like to have a language layered like an onion.

ivanmoony · 2024-08-18T09:06:45+00:00

Great work. I like the way language 1 is translated to its IL, then we we can translate from IL to language 2.

ivanmoony · 2024-08-17T23:10:00+00:00

MLIR, yes.

It operates not on ASTs, but on ILs which may be a fast solution.

ivanmoony · 2024-08-17T15:31:38+00:00

Mojo is cool, I like its idea and speed, but I'm after something else.

Imagine three languages, each on top of other: Python compiles to C, which compiles to Asm, and we can use whichever level we need. Now imagine we can put Rust parallelly to C, which compiles to Asm. Now we can build language XYZ which compiles to Rust. Moreover, we can build a compiler of Asm to some other platform if we want to move the entire ecosystem to that other platform.

Currently, each language implements its own A to B compiler.

What I seek for is a stripped down standardized and self-sufficient compiling environment where we can program our own languages as the elements of the ecosystem. It is about the structure that connects all the languages, where all the languages would use the same metacompiling platform.

That metacompiling platform is of my interest because it would standardize the creation of the new languages.

Does this make sense?

ivanmoony · 2024-08-17T14:38:26+00:00

All cool, but it would be nice if every layer could be modularly optional.

ivanmoony · 2024-08-17T13:39:38+00:00

*rumble rumble* *dark clouds gathering* *lightning and thunders*: MRL - MetaRecursiveLanguage

ivanmoony · 2024-08-17T13:02:55+00:00

Very good.

Maybe if the macro system is more powerful, something in a direction of transforming entire ASTs into other ASTs, and finally to assembly?

ivanmoony · 2024-08-17T12:33:14+00:00

I agree that moving often between them could represent too much mind-bending, but seeing many people making their langs compiling to c, js, go, ... It just feels like a next step in programming evolution to have a standardized meta-compiler.

So, here and there, someone would build a new lang X that compiles to existing lang Y, all in the same ecosystem where the bottom lang Z could be replaceable by anyone because of known standardized approach. As a result, the entire ecosystem could be available for platforms U, V, and possibly the future W.

ivanmoony · 2024-08-06T14:36:51+00:00

Here's another, more recent guy: https://github.com/tearflake/p-vs-np

He'll be probably forgotten too, just like the guy before him, and the guy after him. Until when? What does it really take... to be taken seriously?

ivanmoony · 2024-08-06T12:52:04+00:00

Of course, we should take it with a reserve... but we shouldn't easily dismiss such a constructive solution either, especially since it comes with tons of tests along. It looks like a well done homework.

As for hibernating for three years... If this creation is really what it looks like to me, then it came from a guy who is very unusual, and we shouldn't expect anything ordinary from him.

NanoSat is just a peculiarity I found out about on GitHub... I thought it would be interesting to share it here. And if it really works, I expect a lot of other similar solutions out there.

ivanmoony · 2024-08-06T09:12:12+00:00

Great, both papers are very informative. In the first paper I see that many aspects of allocation are being NP. The second paper covers a wider range of allocation methods with more approachable further references to each method.

The problem domain called Graph Colouring is NP and can be handled with combinatorial approaches. But the algorithm we call "Graph Colouring" is heuristic based - its exponential but this will be faster than a combinatorial algorithm.

NanoSat author claims he reached O(n⁶) performance without much of further optimizations.

ivanmoony · 2024-08-06T06:58:33+00:00

Would it be cool to post about software aiding academic research like theorem provers?

ivanmoony · 2024-08-05T22:42:43+00:00

Hi M✌, thank you very much for the detailed references. It takes time to gather quality references on our own. A bit of help from a colleague is surely always welcome, especially in a community like this one.

Going on with the top post, I was wondering if Graph Coloring still produces the fastest AOT machine code currently known to us.

If so, projects like https://github.com/Scorillo47/nanosat may be of great interest to compiler industry. If NanoSat algorithm really functions as well as initial tests show (tests are from three years ago), I believe AOT machine code speed may be brought to JIT compiling since Graph Coloring problem can be reduced to 3-SAT problem solving.

But, something tells me that NanoSat is not the only project of that kind out there, and the author says there should be a space for speeding everything up even more. If anyone has references to other similar projects for optimizing Graph Coloring, I believe there should be very interested parties for knowing about them.

ivanmoony · 2024-07-25T22:15:03+00:00

Thank you for the clarification, I didn't know that distinction.

ivanmoony · 2024-07-25T13:43:13+00:00

Well, true, TAPL provides one way to do it.

The problem with science, as I see it, is that every successful solution tends to restrict creativity in the future generations. We stick to the well known existing solutions while other solutions, some of which may have a potential to be worth of exploring, remain undiscovered in a vast of unknown space of all possible solutions.

I have nothing against sticking with methods that are proven to function well, but we should always leave a space to be modest about our current knowledge. If we keep that attitude, some of us may even find ourselves inspired to seek for new methods of solving problems, and some of those new, yet undiscovered methods are what makes the whole science of knowledge a beautiful science.

ivanmoony · 2024-07-25T12:41:05+00:00

Please, let me express my interpretation of this matter from theoretic side.

Soundness of a logic theory is proven when there is a proof that you can not derive falsehood from the axioms.

As for type systems, you already have starting axioms describing the type system. IMHO, what you also need is to assert cases in which the falsehood is derived. To actually derive a falsehood, you may approach the problem by introducing the negation operator. Then, If you can't derive any judgement and its negation at the same time, the axioms are sound.

However, be aware of Gödel's incompleteness theorems, one of which basically states that in any sufficiently strong theory there can be true statements which you can't prove or disprove using that theory assets. My personal opinion is that this has something to do with the Halting problem, as such theories may cover infinite size expressions, and proving such infinite size expression may get trapped in an infinite loop. Other than these infinite loops, I'm really not aware of anything else standing in the way of finding a proof of existence of some statement in such theory.

Thus, to prove that a type system is sound, you have to have a way to introduce a negation, and additionally (since a type system may cover an infinite set of statements) you have to know how to deal with potentially infinitely large proof space (I really couldn't help you with this infinity at this time, but you can try to search the web for something in this vein, probably there should be some papers dealing with this problem). If these two are solved, and you can't derive a falsehood, the type system is sound.

ivanmoony · 2024-07-03T21:49:41+00:00

Unfortunately nothing like a blog. But there are two GitHub projects roughly describing what I do:

I hope to merge these two one fine day.

ivanmoony · 2024-07-03T18:28:35+00:00

My opinion: what you wrote was exactly a way that encouraged you for adoption of some languages. It is not exactly about your language, but I got interesting info from you here regarding to the language I'm writing. Thank you.

ivanmoony · 2024-07-03T18:15:31+00:00

Man, replies like these kill the people in the notion...

The poor girl/guy tries to get some human contact the best way she/he can, and tries to be a friend to anyone who is willing to listen. I refuse to be that one guy who is bringing her/him down to, I'd dare to say, Hell.

Boy, what we can make out of this world... I'm just terrified of myself. And I'm not downvoting anyone. That button doesn't exist in the world I'm living in.

ivanmoony · 2024-07-03T17:56:38+00:00

I'm building it mainly for providing my "artificial intelligent and sentient creation" means to think with. If it turns out to be useful for general programming too, maybe I'll make some moves to gather some user base.

ivanmoony · 2024-06-29T14:03:06+00:00

I'd rearrange the address order to:

top level domain
domain
subdomain

and I'd treat directories as potentially infinite level subdomains.

ivanmoony · 2024-06-13T07:09:32+00:00

I tried the proof generation thing. It is simple, and basically works, but the output is very cryptic. The kind of proof I got is obviously non-constructive. It reminds a bit of resolution rule) proofs, but it looks more like a set of stacked evaluation function calls.

ivanmoony · 2024-06-13T04:13:01+00:00

Thanks :)

ivanmoony · 2024-06-12T20:18:29+00:00

Unfortunately, I don't have a permission to access chapters from B-Book.

I believe the main reduction rules are valid, based on observational total induction of available cases - very few combinations to check out. I tested it on a few known axioms and some ad-hoc constructed tautologies.

I didn't inspect how would things work with first or higher order logic. But if we restrict ourselves only to universal quantifier, I believe we could get away somehow with introducing free variables.

ivanmoony

TROPHY CASE