The Hare programming language • Hacker News Board

Re: The Hare programming language

#161

Post by lifthrasiir » Mon, Apr 25, 2022, 1:49 PM UTC

jstimpfle wrote: post #143

lifthrasiir wrote: post #89

Earlier quoted context omitted.

> There is a trend among security professionals, as it were, to place anything on the chopping block in the name of security. I really have to disagree on this, in spite of not being a security professional, because the history has proven that even a single byte of unexpected write---either via buffer overflow or dangling pointer---can be disastrous. Honestly I'm not very interested in other aspects of memory safety,…

History has also proven that every little oversight in a Wordpress module can lead to an exploit. Or in a Java Logger. Or in a shell script. And while maybe a Wordpress bug could "only" lead to a user password database leaked but not the complete system compromised, there is a valid question which is actually worse from case to case. Point is just that from a different angle, things are maybe not so clear. Software w…

Two out of your three examples are independent to programming languages. Wordpress vulnerability is dominated by XSS and SQL injection both of which are natural issues arising from the boundary of multiple systems. Java logger vulnerability is mostly about the unjustified flexibility. These bugs can occur in virtually any other language. Solutions to them generally increases the complexity and Hare doesn't seem to significantly improve on them over C probably for that cause.

By comparison memory safety bugs and shell script bugs mostly occur in specific classes of languages. It is therefore natural to ask for new languages in these classes to pay more attention to eliminate those sort of bugs. And it is, while not satisfactory, okay to answer in negative while acknowledging those concerns---Hare is not my language after all. Drew didn't, and I took a great care to say just "not a good response" instead of something stronger for the reason.

Re: The Hare programming language

#162

Post by throwawaymaths » Mon, Apr 25, 2022, 1:49 PM UTC

kaba0 wrote: post #112

throwawaymaths wrote: post #59

Earlier quoted context omitted.

Maybe be less zealous and aware of your assumptions? Your assumption is that memory safety has to be baked in the language. It could be baked into proof assistants that are part of (optional or add-on) tooling, like what sel4 does. A simpler language makes this more possible, and the things that a proof assistants can do go far beyond what rust is able to provide, without sacrificing compilation speed or other forms…

> A simpler language makes this more possible This is false. Rust’s borrow checker is nothing else but an included proof assistant for rust code. The reason it can catch so many memory issues and data races is specifically due to a more restricted language. Also, sel4 is a relatively tiny program which was written for an unusually long time by domain experts. Formal verification simply doesn’t scale to global propert…

> Formal verification simply doesn’t scale to global properties

This is an assertion you are making with absolutely no evidence, and also totally self-contradictory with your statement "Rust’s borrow checker is nothing else but an included proof assistant for rust code".

While we're at it, also Ada does this, which has long been used for large scale mission critical applications where formal assurances are necessary (with even more available optional safeties than rust provides).

Re: The Hare programming language

#163

Post by throwawaymaths » Mon, Apr 25, 2022, 1:52 PM UTC

HelloNurse wrote: post #148

throwawaymaths wrote: post #59

Earlier quoted context omitted.

Maybe be less zealous and aware of your assumptions? Your assumption is that memory safety has to be baked in the language. It could be baked into proof assistants that are part of (optional or add-on) tooling, like what sel4 does. A simpler language makes this more possible, and the things that a proof assistants can do go far beyond what rust is able to provide, without sacrificing compilation speed or other forms…

"Optional" means unused or misused until proved otherwise. No checking and no guarantees can be assumed, and if someone tries to deploy an add-on proof assistant I'd expect managers to see programmers who waste time pursuing some warnings instead of making progress on new features.

This is wholly unimaginative, there is a wide window of usage patterns that are not "unused or misused", for example, on by default but off with a project flag, or off when building a dev release but on when building a prod release, and also don't forget my point that many projects simply don't need the level of memory safety that rust provides. For example if you are single threaded and never free, or if you have an arena strategy.

Re: The Hare programming language

#164

Post by kristoff_it » Mon, Apr 25, 2022, 1:59 PM UTC

FrozenVoid wrote: post #95

Lack of macros in recent systems languages like Zig/Hare/etc seems to be a design flaw, a handicap marketed as safety feature or bargain for clarity. If a language can't replace C macros, it cannot replace C.

You might want to learn more about Zig's comptime.

Re: The Hare programming language

#165

Post by turminal » Mon, Apr 25, 2022, 2:13 PM UTC

eatonphil wrote: post #155

turminal wrote: post #149

Earlier quoted context omitted.

Yes There is one more significant (but not user-visible) change planned for the language before we continue working on that.

What is that?

Code dealing with tagged union matching is going to be completely rewritten and support added for match exhaustiveness checks and matching on pointers to tagged unions without copying the tagged union and its values.

The ability to do the latter is expected to result in a significant performance improvement and stack usage decrease.

Re: The Hare programming language

#166

Post by sanxiyn » Mon, Apr 25, 2022, 2:19 PM UTC

ninjin wrote: post #140

staticassertion wrote: post #137

Earlier quoted context omitted.

The license seems straightforward. You can use and distribute software written in Hare, but if you want to link or make changes to the tooling (compiler, etc) you must open source those.

Yes, legally it is perfectly clear. Just not the why . Is there any other language that has taken a similar approach? Has this been discussed in relation to Hare somewhere apart from the brief chunk of text that I linked? I am perfectly accepting that I may be in error here in terms of how I view licensing, but it bothers me that I can not build a mental model of the intentions of the authors.

It seems basically equivalent to gcc/glibc, which I think is a good default.

Re: The Hare programming language

#167

Post by electroly » Mon, Apr 25, 2022, 2:23 PM UTC

ninjin wrote: post #126

Happy to see “secretlang” out in the open! I have been following development from afar and really like the idea of a “simple” take on a language, but with a lot of wisdom and affordances added since the state of the world back in 1972. In short, Hare seems to be a language that I really should like and I want to take it for a spin. What I find a bit confusing though is the licensing. I belong to the “BSD school”, but…

This licensing regime is copied almost directly from GCC. The compiler part is GPL and the part that gets embedded into your program isn't. GPL-licensed compilers need to do some kind of dance to allow the outputs from the compiler to be free of GPL restrictions, because typically some components distributed with the compiler are linked into the executable. In this case it's the standard library, so the standard library is MPL instead of GPL. Nothing to be concerned about here. I don't see anything unusual on this page.

Re: The Hare programming language

#168

Post by butterisgood » Mon, Apr 25, 2022, 2:26 PM UTC

FrozenVoid wrote: post #95

Lack of macros in recent systems languages like Zig/Hare/etc seems to be a design flaw, a handicap marketed as safety feature or bargain for clarity. If a language can't replace C macros, it cannot replace C.

I don't think many Zig programmers miss C macros. Comptime is extremely powerful.

Re: The Hare programming language

#169

Post by ncmncm » Mon, Apr 25, 2022, 2:28 PM UTC

eatonphil wrote: post #144

It looks like self-hosting is still WIP. Do I have that right? * https://git.sr.ht/~sircmpwn/hare/tree/master/item/cmd/harec * https://git.sr.ht/~sircmpwn/hare/tree/master/item/hare * https://harelang.org/blog/2021-03-14-a-self-hosting-toolchain/

Self-hosting is a very last-millennium form of wankage. Back then, a compiler was a pretty significant program, and compiler construction tools weren't mature.

Nowadays, self-hosting your compiler doesn't demonstrate much of anything. It takes a lot more than a compiler to prove anything meaningful about your language. Time spent on self-hosting is mostly just time wasted. It mainly suggests you were not really serious.

Make a front end for LLVM, and get on with things.

Re: The Hare programming language

#170

Post by zozbot234 » Mon, Apr 25, 2022, 2:32 PM UTC

throwawaymaths wrote: post #162

kaba0 wrote: post #112

Earlier quoted context omitted.

> A simpler language makes this more possible This is false. Rust’s borrow checker is nothing else but an included proof assistant for rust code. The reason it can catch so many memory issues and data races is specifically due to a more restricted language. Also, sel4 is a relatively tiny program which was written for an unusually long time by domain experts. Formal verification simply doesn’t scale to global propert…

> Formal verification simply doesn’t scale to global properties This is an assertion you are making with absolutely no evidence, and also totally self-contradictory with your statement "Rust’s borrow checker is nothing else but an included proof assistant for rust code". While we're at it, also Ada does this, which has long been used for large scale mission critical applications where formal assurances are necessary…

Formal verification doesn't scale to global properties in the general case. Global properties that are simple and type-like (in that they match the syntactic structure of the program in a fully "compositional" way, like Rust lifetimes) can be checked with comparable ease. Complex properties can often be checked within a single, self-contained, small-enough program module. Trying to do both at the same time - check complex properties globally - is highly problematic. That's why the Rust borrow checker has to make simplifying assumptions, and use 'unsafe' as an escape hatch.