Show HN: Ironwall, a safety-first native programming language and compiler

16 points by bOZbfU4YdRnJQ ↗ HN
Hi HN,

I have been working on a new programming language and compiler.

Website: https://ironwall-lang.dev

GitHub: https://github.com/3WyUFvDOdCbBw7gOZHwcfgKF/ironwall

Why a new language is still needed: https://ironwall-lang.dev/en/motivation

The compiler is written in TypeScript at the moment, and work on a self-hosting compiler written in Ironwall is ongoing.

I would be interested in feedback.

Thank you.

12 comments

[ 5.7 ms ] story [ 35.3 ms ] thread
Vouched. This looks like an interesting project noteworthy enough for HN.
I'm not sure most systems programmers would agree that a language with GC is suitable for their work.

"No syntactic sugar" and "no macros" sounds like a recipe for boilerplate that will be offputting for many.

Please consider adding some code samples to the front page of documentation, as syntax can be important to people.

I disagree with some other details, but I do think that a low level GC language that doesn't have some of Go's particular warts (particularly nil and error checking) is worth pursuing.

Writing the initial compiler in Typescript is an interesting choice but I suppose that won't matter after it's bootstrapped.

Ultimately it's hard for me to take the project seriously at such an early stage but I don't think it's fundamentally flawed. Good luck

Currently, this compiler is not at such an early stage. There’s no need to post any code samples on the website right now. If you’re willing to try the compiler, just dump the spec packaged with the release into the LLM and let the LLM write the code.
My feedback is that both the motivation and the language looks like someone who is confused about several concepts in programming languages.

Safe Rust cannot cause undefined behavior ... static systems do not need to predict all runtime paths, presumably referring to the halting problem and Rice's theorem (or whatever the author intends this to mean, the writing is unclear): these systems prove properties for all accepted programs under a conservative model, which covers all allowed programs within the subset admitted by the model.

The guarantee that Rust provides are sound, and the claim depends on trust in compiler implementation and any `unsafe` code involved in used APIs, etc (which is not uncommon: the same thing is true for Lean's kernel, for instance).

As Pauli said, much of the writing is not even wrong ... many of the language critiques read like transcriptions of vibes derived from AI discussion: "C++ smart pointers with extra steps" -- this is not a serious statement. I'm not even a serious user of Rust, but I know enough about the language design to understand how stupid this statement is.

So the goal seems to be: Java, but without nulls, erased generics, OOP, or the JVM.

Best of luck.

You are projecting your own misunderstandings and confusion onto others.

Calling safe Rust “sound” is meaningless at best and misleading at worst. You cannot seriously test soundness without a formal model and a complete, stable list of undefined behavior. full safe Rust has no formal model, no complete stable list of undefined behavior, to assert that full safe rust is sound is absurd to begin with. keep "not even wrong" to yourself. Is your understanding of Rust’s soundness based entirely on wholehearted belief in Rust’s advertising claims, without even the slightest examination?

“Safe Rust is sound” is an outrageously false claim.

The claim that the guarantees Rust provides are sound is a false claim on the level of a declaration announcing the invention of a perpetual motion machine. You are not merely repeating Rust’s advertising claims; you are producing an absurdly strengthened version of them, claiming that “the guarantees Rust provides are sound” — a statement that even the rust-lang.org front page does not dare to make.

The closest thing one can find right now that is related to proving Safe Rust sound is RustBelt.

The language RustBelt claims to prove properties about is a rust-LIKE language, an APPROXIMATION to a subset of Safe Rust, with a SIMPLIFIED memory model. There is a HUGE GAP between that and the actual memory model.

RustBelt certainly did not prove that a subset of Safe Rust is sound, let alone full Safe Rust.

There is simply no proof anywhere that full Safe Rust is sound.

Rust’s advertisements — original text:

1. “No matter what, Safe Rust can’t cause undefined behavior.”

2. “Rust’s rich type system and ownership model guarantee memory safety and thread safety, enabling you to eliminate many classes of bugs at compile time.”

The first one is outrageously false claim.

The second one is another outrageously false claim. The funny part about the second claim is that array bounds checking is part of memory safety, yet it is handled by a runtime mechanism, not purely by the type system and ownership model as advertised.

These days, Rust memory-corruption CVEs are easy to find online. Given how obvious and readily available the evidence is, it is astonishing that they still have the audacity to make such an outrageously false claim: that “Rust’s rich type system and ownership model GUARANTEE memory safety and thread safety — enabling you to eliminate many classes of bugs at compile time.” The claim is not only easy to see through at a glance, but also contrary to basic engineering intuition. Yet the truly bizarre part is that many people actually believe it, even though the counterevidence is extremely easy to find.

Anyone with even a modest amount of real-world software-engineering experience—so long as they still retain a basic instinct for practical engineering, not necessarily exceptional talent or deep expertise—would, upon hearing that a practical subset of a practical programming language has been proven sound, immediately feel as though they were being sold an absurd perpetual-motion-machine claim. And yet, the whole industry remains indifferent toward Rust’s outrageously false claim.

In a practical engineering language, constructing a safe subset whose soundness can be proven is trivial. The hard part is constructing a PRACTICAL subset of the language that can also be proven sound. For now, this task seems hopeless.

Considering that full Safe Rust has never been proven sound, is the safe region of Rust really a PRACTICAL subset of Rust? I do not think so. It is clear that Safe Rust does not have enough expressive power to write arbitrary code, which is why there are so many unsafe regions and chained unsafe dependencies across the entire Rust ecosystem.

There are three problems:

1. Array out-of-bounds safety 2. Memory safety 3. Concurrency safety

Each problem is at least an order of magnitude harder than the previous one.

What is Rust’s strategy for handling these problems?

For array out-of...

I feel like your charactization of Rust is based on a misunderstanding. Safe Rust does not rely on predicting every future execution path, nor on understanding all runtime states. Safe Rust relies on making it provably impossible to take an execution path or reach a runtime state that is unsafe. This is a completely, entirely distinct approach and is not anything like existing static analyses e.g. of C. In fact that very drawback of being "forced to change otherwise natural data structures and API designs" is exactly for when you cannot sufficiently prove they are Safe Rust.

Since you are not a fan of that, of course Rust may not be for you. But to pose it as an issue of unattainable static analysis is incorrect. Safe Rust achieves the analyses it does because it simply does not have constructs that require knowing every execution path or every runtime state. Its safety does not depend on that. You can choose to depend on it in Unsafe Rust, but then the soundness of that will depend on you, the programmer, rather than on the language.

Before accusing others of misunderstanding, do a little research yourself. Don’t wholeheartedly believe ads without examining them first.
Ads? I've been using Rust since 2020. My last job was in Rust.

I accuse you of nothing, I only wanted to clarify.