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

Show HN: Micro-mitten – Research language with compile-time memory management

github.com

Post reply on HN
Print view View original

61–68 of 68 posts

Re: Show HN: Micro-mitten – Research language with compile-time memory management

#61

Post by MaxBarraclough »

Ono-Sendai wrote: post #25
myu701 wrote: post #14

If a language like this were to take off, I could see linter-style errors pop up that are not currently possible. "ERROR: maximum memory usage computed to be XYZ MB, which is higher than the speicified limit of 500MB" Now that would help keep the RAM bloat down!

My functional language Winter has errors like that. You can compute the maximum memory usage of the program and then throw an error if it exceeds some threshold. Edit: I'll add that there are lots of programs the prover can't effectively handle right now, so can't compute a good memory bound. It works fine for some relatively simple programs however.

> there are lots of programs the prover can't effectively handle right now

And always will be, due to Rice's Theorem. Can still be useful though - various formal methods techniques are like this.

Re: Show HN: Micro-mitten – Research language with compile-time memory management

#62

Post by edjroot »

iknowstuff wrote: post #43
amelius wrote: post #40

I'm thinking that until they are perfect these kind of languages lure the developer into a one-way street, convenient until you reach a dead-end at which point your only escape (if you are lucky) is a whole bunch of contrived and difficult to maintain typing constructs. Still interesting research though.

Your comment carries very little substance (reads like a baseless opinion) but appears on the very top of the page. Interesting.

At least according to [1] and [2], comment order is not determined just by the comment's score but also by the posters', when it was posted, and other things.

[1] https://news.ycombinator.com/item?id=1398764

[2] https://news.ycombinator.com/item?id=13867739

Re: Show HN: Micro-mitten – Research language with compile-time memory management

#63

Post by im_down_w_otp »

myu701 wrote: post #14

If a language like this were to take off, I could see linter-style errors pop up that are not currently possible. "ERROR: maximum memory usage computed to be XYZ MB, which is higher than the speicified limit of 500MB" Now that would help keep the RAM bloat down!

You can already do this with certain forms of type-level programming. We did it in the Rust-based OS we created atop seL4. It started out as using types to track setup processes and kernel objects at compile-time to bring some of the guarantees seL4 provides only at run-time, and also to provide guard rails to ensure that you're not accidentally creating unsecure systems using the tools seL4 gives you. After some exposure to doing this it became clear that we could also track memory allocations this way, so we created an allocator to do exactly that.

It basically ensures at compile-time that every allocation in the program will succeed given some expected usable footprint, which also has the benefit of ensuring that we kill the kernel/OS immediately at bootstrapping if the machine/environment doesn't have enough memory to make sure our proof-carrying code can meet its expectations.

One huge problem with this approach though is that it doesn't scale well. Where "scale" is in the dimension of revising your programs because the type-parameters tend to bleed all over the place and don't compose well/at-all. So, it's great if you're sure you've got your design locked-in, but it's kind of a nightmare if you're still prototyping & refactoring.

Re: Show HN: Micro-mitten – Research language with compile-time memory management

#64

Post by pjmlp »

YetAnotherNick wrote: post #35
_bxg1 wrote: post #18

Earlier quoted context omitted.

As long as it still allows for arbitrary-length vectors - which I can't imagine it not - this would be impossible due to the halting problem. Or I guess, maybe you could derive a lower bound on memory usage, but you could not get an upper bound/exact number.

What about allocation is only possible when you can prove the upper limit. So this is possible if (sz (sz) else throw "Size exceeds upper limit"

This is Ada behaviour when doing stack allocations actually.

Re: Show HN: Micro-mitten – Research language with compile-time memory management

#65

Post by pjmlp »

_bxg1 wrote: post #46
wtetzner wrote: post #39

Earlier quoted context omitted.

Maybe there could be a compiler flag. You let any program compile normally, but if you enable the flag, it only allows programs to compile if the maximum memory usage can be computed, and if there are under the limit you specify. That means the language isn't always crippled, but you can get compiler enforcement for certain embedded programs.

It would effectively become a stack-only language (heap allocations' sizes would always have to be known at compile time, just like on the stack). I could see that serving an interesting special subset of use-cases, but I was under the impression we were talking about a general programming language, which that would not be.

Ada/SPARK does not allow for dynamic allocations, all of them must be proven at compile time.

Re: Show HN: Micro-mitten – Research language with compile-time memory management

#66

Post by Ono-Sendai »

MaxBarraclough wrote: post #61
Ono-Sendai wrote: post #25

Earlier quoted context omitted.

My functional language Winter has errors like that. You can compute the maximum memory usage of the program and then throw an error if it exceeds some threshold. Edit: I'll add that there are lots of programs the prover can't effectively handle right now, so can't compute a good memory bound. It works fine for some relatively simple programs however.

> there are lots of programs the prover can't effectively handle right now And always will be, due to Rice's Theorem. Can still be useful though - various formal methods techniques are like this.

Winter is not a Turing equivalent language, so technically Rice's theorem doesn't apply (I think). Nevertheless practically speaking you are right, there will always be valid programs that the prover can't prove are correct.

Re: Show HN: Micro-mitten – Research language with compile-time memory management

#67

Post by [deleted] »

pietroppeter wrote: post #15

might be worth knowing that there is a production-deployed programming language which - besides being a great language in many, many respects - will very soon (next release) have compile-time memory management (already working and performant for stdlib including async) in a stable release: Nim. [1] https://forum.nim-lang.org/t/5734#35562 [2] https://forum.nim-lang.org/t/6125#37829

[deleted]

Re: Show HN: Micro-mitten – Research language with compile-time memory management

#68

Post by pietroppeter »

pietroppeter wrote: post #15

might be worth knowing that there is a production-deployed programming language which - besides being a great language in many, many respects - will very soon (next release) have compile-time memory management (already working and performant for stdlib including async) in a stable release: Nim. [1] https://forum.nim-lang.org/t/5734#35562 [2] https://forum.nim-lang.org/t/6125#37829

Yep, made a comment without really knowing the subject. Can I downvote it too? :P
Post reply on HN