Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Hare programming language

harelang.org

Post reply on HN
Print view View original

171–180 of 323 posts

Re: The Hare programming language

#171

Post by eatonphil »

ncmncm wrote: post #169
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 serio…

> Self-hosting is a very last-millennium form of wankage

You're reading way more into my comment than I wrote. I asked a question.

Re: The Hare programming language

#172

Post by onlyrealcuzzo »

lloydatkinson wrote: post #51

Why do people keep choosing :: over simply .? How does adding more visual noise help anyone?

To distinguish between an instance and a namespace?

The same can be said for why do we need to put parenthesis after functions that take no parameters? So people still know it's a function.

Re: The Hare programming language

#173

Post by FrozenVoid »

BaculumMeumEst wrote: post #106
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.

What necessary use case of macros isn’t addressed by comptime in zig?

zig comptime is the same as constexpr/consteval in C++ which operate on variables and valid code blocks.

C macros operate on arbitrary tokens, which get converted to code or constants. For example variadic functions can be implemented to act on token arglists that act as abstract tuples: https://github.com/FrozenVoid/C-headers/blob/main/argmanip.h

Re: The Hare programming language

#175

Post by kaba0 »

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…

I meant to write every global property due to Rice’s theorem.

And I don’t believe my claim is unsupported, the largest formally verified program is the mentioned sel4, which is still tiny compared to even the smallest of business apps and was written by domain experts over multiple years.

Restricting a problem to a subset is like the numero uno step to solve any hard problem - and this is what rust basically mandate. It won’t provide bug-free programs, but it can reliably prove the absence of memory bugs and data races due to the borrow checker, which can do its work on function-scope, since all the relevant information is encoded in the function’s generic lifetime arguments.

Re: The Hare programming language

#176

Post by metaltyphoon »

ddevault wrote: post #28
xeeeeeeeeeeenu wrote: post #26

Not supporting Windows and macOS will likely hurt the adoption of the language. Anyway, is it possible to target bare-metal with Hare? Is it possible to use it without the standard library?

> Not supporting Windows and macOS will likely hurt the adoption of the language. Not among our target audience it won't. > Anyway, is it possible to target bare-metal with Hare? Is it possible to use it without the standard library? Yes. Here are two kernels written in Hare that don't use the stdlib: https://git.sr.ht/~sircmpwn/helios https://git.sr.ht/~yerinalexey/carrot

> Not among our target audience it won't.

Yes it will. I have no interest in using Linux as desktop but I do use it for deployments. If there is one trait of major PL is the adoption of the big 3 OSes.

This is Hare’s biggest flaw right now.

Re: The Hare programming language

#177

Post by ncmncm »

The first thing I look for in something that claims to be a systems language is whether it provides anything that helps me out.

First and foremost, does it provide any primitive that can be used for automation? C++ brought destructors, Rust did a Drop trait. What do you have?

Second, does it provide any way to operate on types? C++ got templates, Rust offers generics. What do you have?

Third, does it provide useful compile-time logic?

If it lacks those, what does it bring to the table to make up for those gaping holes? This is not the '70s, or even the '80s. We have learned things since then. Have you?

Re: The Hare programming language

#178

Post by staticassertion »

zozbot234 wrote: post #170
throwawaymaths wrote: post #162

Earlier quoted context omitted.

> 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 c…

I'm not really convinced that this is true. I think you're brushing up against Rice's theorem, which is that proving arbitrary properties about arbitrary programs is equivalent to the halting problem. That's why we constrain languages with type systems, which limits any typed language from expressing arbitrary turing complete programs.

Proof assistance is sort of irrelevant. Types and proofs are related, as denoted by the curry howard correspondance.

The real issue with "throwawaymaths"' point is that they're saying "use proof assistants" to people who are using proof assistants. SEL4 is a terrible example of a success story, as it took ages to complete, and then there was immediately a bug found in a class they weren't looking for - because rice's theorem.

They're clearly advocating for the use of specific and explicit proof assistants, which is fine and a totally reasonable thing to advocate for, but in no way is related to rust or the discussion, which is why I chose not to engage.

Re: The Hare programming language

#179

Post by amelius »

ncmncm wrote: post #177

The first thing I look for in something that claims to be a systems language is whether it provides anything that helps me out. First and foremost, does it provide any primitive that can be used for automation? C++ brought destructors, Rust did a Drop trait. What do you have? Second, does it provide any way to operate on types? C++ got templates, Rust offers generics. What do you have? Third, does it provide useful c…

> We have learned things since then. Have you?

We have learned to read the documentation before we judge things.

Re: The Hare programming language

#180

Post by FrozenVoid »

butterisgood wrote: post #168
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.

C macros are powerful enough to create entire functional languages at compile time, which is far beyond any constexpr functions. https://github.com/rofl0r/order-pp
Post reply on HN