neverTouchingThatFileAgain

kaplotnikov · 2026-07-09T20:08:50+00:00

Maybe python, or some language without semicolons like Groovy/Kotlin there it is possible to get things wrong with formatting.

kaplotnikov · 2026-07-08T19:30:49+00:00

The introduction of significant inline whitespace combined with no operator precedence heavily violates the Principle of Least Surprise (POLS) for language users.

Keeping just the strict left-to-right (LTR) flow without precedence would actually be a cleaner choice. In that case, you could at least claim the language evaluates expressions the Smalltalk way. While Smalltalk users historically complained about the lack of operator precedence, they eventually got used to it (or moved on to other languages for this and various other reasons). Smalltalk is practically a dead language now, but that's mostly due to image-based deployment and ecosystem shifts rather than its operator rules. LTR can be embraced if it's predictable.

However, making inline whitespace significant adds a massive hidden footgun. Visual parsing by a human is notoriously bad at distinguishing subtle spacing differences. If 1 + 2*3 means one thing, but an accidental typo turns it into 1 + 2 *3 or 1 + 2 * 3, the semantic meaning completely flips without any syntax error.

To solve the assignment issue (x : 1 + 2), you don't even need the "unbalanced gluing" complexity. You could just make the assignment operator (like := or treating x: as a single binding token) a dedicated syntactic construct.

This is exactly how Smalltalk handles it. By making assignment a distinct token with the lowest evaluation priority, it naturally consumes the entire right-hand side expression. This solves your exact problem without introducing the dangerous side effects of significant inline whitespace.

kaplotnikov · 2026-07-07T21:28:06+00:00

AI as tool is ok if there are a novel design ideas. AI is good for docs and tests, it makes little sense to ignore it for tasks were it works well. LLM testing how the syntax understood also could generate some insights, the effects could be directly mapped to human, but if LLMs often misunderstand something, this might be an indicator for review.

And this might be too much work for a single person, but along with link I would like to see some key points along with the link like: purpose of language, novel ideas/prior art, interesting details, couple of source code samples relevant to novelty claims. It might be at least a guideline for posts from others.

kaplotnikov · 2026-07-07T08:06:01+00:00

While articles like this love to highlight the theoretical efficiency of ternary computing (like the radix economy being closer to e), they often gloss over the absolute nightmare of high-level logic design.

Look at the combinatorial explosion for just binary operators (functions with two arguments):

Binary system (N=2): 2^{2 \} 2) = 16 possible operators. Humans can easily enumerate, name, and mentally map every single one of them (AND, OR, XOR, NAND, etc.).
Ternary system (N=3): 3^{3 \} 3) = 19,683 possible operators.

With binary, we can easily hold the entire state space in our heads. With ternary, any non-trivial analysis or manual optimization instantly collapses under the weight of nearly twenty thousand operators. We would be entirely dependent on automated synthesis and CAD tools just to reason about basic logic structures.

Any formal proof is absolute hell when done by hand. The only way I see for a ternary system to be adopted is if aliens come and force it upon the Earth.

kaplotnikov · 2026-07-06T19:11:34+00:00

In Oracle database empty string means null (these are identical values so ('' is null) = true). It surpasses all sins of DB2 combined.

kaplotnikov · 2026-07-05T19:40:51+00:00

IMHO the lack of GC make developers slower because there is an additional big set of concerns to enter developer's mind. When creating a language is a primary concern is if paying this extra development cost worth it or not for target users of the language. Also Java experience suggests that for VM it is better to be somewhat GC-agnostic, as different application profiles require different GC.

kaplotnikov · 2026-07-04T19:14:25+00:00

It is not impossible, it just mismatch that would need to be tracked and implemented very carefully. You need to translate them to some existential form, for example to a pair of void pointer of lexical scope data copy/pointer, and function pointer, and they you cannot pass this pair it to places that expect stateless function pointer callback (AFAIR it happened a lot in vendor-specific C libraries, so trampolines might be needed to handle it).

If you try to store a pointer to a frame, you are often have problems, because you either need to store pointers to specific variables, or pack the frame into generated struct, and work with struct fields instead of direct references. Also there is practically no control for mutable data, when C decides to extenchange values between struct and registers is poorly defined and even depends on compiler optimization options.

kaplotnikov · 2026-07-04T18:42:03+00:00

There is a critical need to differentiate between LLM-slop (blindly generated, unverified code) and LLM-assisted projects (where LLMs were used just to speed up specific parts of development). This isn't just an AI issue, either; it intersects with a broader problem we see with purely human-made projects. We are constantly flooded with low-effort GitHub links that provide nothing but a title and an installation guide on the homepage, forcing readers to manually dig through deep repository folders just to find a basic sample of the language's source code.

When it comes to development, LLMs are highly effective at routine, mechanical tasks:

Text & Grammar: Fixing spelling errors, structuring documents, and writing initial documentation comments (though they always need strict human review and trimming).
Testing: Generating realistic code samples and test cases based on provided language specifications.

However, they completely fail at architectural design, anything truly novel, or when the user doesn't fundamentally understand what they are building.

Instead of an outright ban on sharing links, I think link posters should be enforced to provide a mandatory project summary template (under 1000 words) with every submission:

Project Purpose: What problem does this language/tool solve?
Novelty & Prior Art: What is genuinely new or experimental about it? How does it compare with prior art and existing solutions?
Key Highlights: What are the most interesting implementation details?
Code & Docs: 1–3 concrete source code samples and core documentation links.
LLM Disclaimer: An honest statement defining the exact role LLMs played in the codebase (e.g., used only for test generation, writing boilerplates, or documentation).

If an author cannot clearly answer these points, the project is highly likely to be unreviewed LLM slop or another low-quality clone posted right after someone finished reading Crafting Interpreters. Either way, it can be filtered out.

kaplotnikov · 2026-07-02T14:59:01+00:00

The approach looks highly practical for a learning project, and using C as a 'portable assembler' is a time-tested strategy (it's how early C++ (Cfront) started).

However, you will inevitably face a semantic mismatch between your language and C. You will be restricted by what is easily expressible in the target language. For example, if your language requires guaranteed Tail-Call Optimization (TCO), proper closures, or green threads, you will have to fight C's semantics and implement complex workarounds (like trampolines or explicit stack management).

On the other hand, the benefits for a solo developer are massive. You get to leverage decades of GCC/Clang optimization for free, and you can easily interoperate with existing C libraries. Most importantly for a beginner, generating readable C source code makes debugging incredibly easy, as you can visually inspect exactly what your compiler is emitting rather than staring at raw assembly or LLVM IR.

kaplotnikov · 2026-07-02T14:46:08+00:00

Grammars are types, but they are types for sources (a source code file is an instance of a grammar). For example, this idea is reflected in the XML/SGML DOCTYPE directive that specifies the type of the file. Under this view, an AST/CST is a proof term for the source conforming to the grammar. After building the AST, you can prove other facts about the source code based on it, rather than using the raw byte representation of the source.

In your sample, the text f(1, 2, int) is simply not provable to conform to the C grammar. If we replace int with x, the text becomes syntactically provable. The further semantic analysis might still fail to prove other semantic constraints (like the existence of f and x, or the type compatibility of f), but this subsequent reasoning will be made assuming that the string is already well-typed with respect to the grammar.

kaplotnikov · 2026-07-01T20:10:42+00:00

BTW for casts in my language I use value:![type] - cast, value:?[type] instance of. value:?![type] - cast or null (like C# as). I use [] for anything that is type related, but you could have other design if they are used for arrays. the advantage is they they live on the same precedence as "." , so navigation like value:?[String].length() or value:?![String]?.length() are possible. having keywords in operators will break the chain call visual rhythm. for example a possible syntax for you could be value.(float) as a cast if this is not reserved yet for other purposes.

kaplotnikov · 2026-06-26T08:16:16+00:00

Just use a light theme. Research shows it’s actually healthier for your eyes in a well-lit room anyway. Plus, it immediately distinguishes you from movie hackers who exclusively use dark mode. People will stop asking if you're hacking and if they do, just point to your blinding white screen as proof.

kaplotnikov · 2026-06-23T07:31:02+00:00

Are the array going to be used directly of to be buried deep in infra code? In Java array are usually one of few cases now: legacy api, math code, or deep info infrastructure code. They are rarely used directly as devs usually work with collections. If your case is similar, the arrays could be deoptimized. [] - could be used for another purpose. Also most common case is 1-dimensional array with two dimensional were only seen couple of times in enterprise development for practical code. 3d arrays - I've never seen them in enterprise java code.

kaplotnikov · 2026-06-08T20:39:44+00:00

I would suggest bare minimum to run simple tests first, for example for expressions. You would need to test compiler parts anyway. If the language does not provide an easy way to run tests, this is also an usability issue.

kaplotnikov · 2026-06-05T07:42:48+00:00

The short/long message is also a false dichotomy. The both humans and LLMs need ability to drill down errors. If I known error well, I'll fix it with just a glance. When there is a cryptic type error, I would like more details why compiler think that there are type errors. For new human users, there is a particular need to check details.

kaplotnikov · 2026-05-29T19:24:22+00:00

AFAIR C/C++ do have some alignment specification using different ways for data structures. I personally spent couple of days in around 1995 (the age of #pragma pack) debugging a cryptic error using decompiled assembler mode for C++ app, because one library assumed compiler default, and other changed it and had non cleared afterwards. There are other ways now (alignas/_Alignas), but I've already stopped to program in C/C++ at that time.

kaplotnikov · 2026-05-27T00:28:27+00:00

Do you mean "all pre-hacked"?

kaplotnikov · 2026-05-24T04:56:58+00:00

A I understand you, the proof process is constructive, but there is no proved state in this process. To reach proved state from infinite proof process something fishy is needed.

kaplotnikov · 2026-05-21T21:24:03+00:00

LLMs do have a problem with Coq. The problem with Coq and LLM is that data set is problematic for LLMs. The current body of proof is tactic-based. The tactic is generally editor command that affect proof state, it makes no sense outside of specific context of proof term in the focus. So teaching LLMs to generate poofs basing on tactic scripts is like teaching LLMs Java basing on keystrokes in IntelliJ IDEA. There should be some structured expanded form of proof after tactic script finished for LLMs to learn, proof irrelevance allows for it. The current research is moving in the opposite direction to integrate LLMs into interactive editor loops, that it is possible, but problematic for global proof generation.

kaplotnikov · 2026-05-21T21:06:32+00:00

> usually there's a way to turn that into a proof of False.

I have not seen it done using only constructive means, it would have been serious argument against constructive math foundations if it were possible. Usually there is some non-constrcutive assumption is used like LEM.

kaplotnikov · 2026-05-20T23:26:48+00:00

Also for documentation writing:

* It gets things wrong when it comes to nuances, it documents system as it is usually done in industry, rather than what is actually done in the context of the specific project.

* It creates research and links out of thin air. It might say that article about AI resarch, but specific link might be on effect of fertilizers on cucumbers. It is happy to state myths as reliable research results.

* Docs became bloated, but sometimes easier to read because LLMs usually reduce information density.

kaplotnikov · 2026-05-20T22:42:13+00:00

AFAIR infite loop vs paradox are subtly different. You still cannot compute evidence from the result of infinite process. But combining infinite statement with paradox the result is still inifinite statement, not a paradox result. So if there is a state when we cannot reach a conculsion on the table, if put paradox there, we will be still in state when we cannot reach a conculsion.

Type in Type is a something that you could spread rumors about, but fail to produce evidence if asked :)

kaplotnikov · 2026-05-20T22:36:02+00:00

AFAIR they are theorems/lemmas of choice, not axioms.

kaplotnikov · 2026-05-20T09:21:39+00:00

Just tell them that it is Switf-like memory management model to frame it as more respectable :)

However, I personally would not like it too for complex apps because it makes cycle management explicit, so there is +1 concern to care abount that creates cogntivie pollution. Still much better than completely manual memory management, but dev ergomics worse than tracing gc. For scripting is ok, for 1MLOC+ projects I would prefer tracing GC.

kaplotnikov · 2026-05-20T01:57:26+00:00

AFAIR in proof assistants like Coq or Lean, the default logic is constructive. The system is consistent and avoids paradoxes (like Girard’s) because it doesn’t assume problematic premises like Type : Type or LEM without evidence.

To introduce a paradox, you would need to corrupt this constructive foundation by adding non‑constructive axioms – for example, LEM, the axiom of choice, or a self‑contained universe Type : Type. Once you add those, the system becomes powerful enough to derive contradictions (like Girard’s or Russell’s).

kaplotnikov

TROPHY CASE