HN user
A gal living at the intersection of high-performance infrastucture, machine learning and PLT. Oh, and a bit of music too.
https://github.com/iamrecursion
I've tended to find a lot of value in systems that have both, especially when there is automatic translation from the simple config to the Turing complete language. Lean 4's lakefiles are a good example of this, with a TOML format that is a subset of the Lean DSL format.
It is unfortunately not possible to have a Base exist without its own file, even if they can be embedded using the standard `![[]]` syntax.
It says this at the top!
I’m very curious as to what you’re working on. Is the language open source?
Not at all. There’s an LLVM bitcode interpreter built on top of GraalVM, but the VM itself is heavily reliant on the internals of OpenJDK.
I’ll echo this recommendation. Peter F. Hamilton is firmly my favourite sci-fi author, and that’s a hard spot to take.
The Commonwealth Saga (mentioned by the parent) is followed by The Void Trilogy and then The Chronicle of the Fallers, all set in the same Commonwealth universe. It’s some of the most evocative writing I’ve ever heard the pleasure to read, and the stories told are massive in scale but without seeming lacking as a result.
My e-reader says that my most recent read-through was my 9th, so add that to a number done with physical books and it should give some idea of how good I consider these books!
I don’t know if nexuist found out about the Essential Air Service the same way that I did, but I learned about it today from the latest Wendover Productions video [0]. A fantastic and informative channel with high production values, if you’re not familiar.
I run an audio engineering business.
At first it was just a project of passion, but years later and a not insignificant investment in gear, software, and other equipment has left me with a side business that nets a tidy bit of income.
It’s also something that I adore doing, and hence a massive plus. I get to mix and master a whole variety of music, from classical to ambient, to EDM, and it’s always a pleasure to work with artists whether they’re new to it all or seasoned professionals.
A good foundation for such a language would be one based on Quantitative Type Theory [0]. It’s a dependent type theory that records usage information in every typing judgement.
The Idris successor, Blodwen [1] is being based on it.
[0] https://bentnib.org/quantitative-type-theory.pdf [1] https://github.com/edwinb/Blodwen
While I do use an Apple Watch, I can second the build quality of Withings’ products. I also use their scales!
This is a beautifully designed site. It manages to tell a coherent narrative in such an engaging way. It’s lovely!
It made me smile to see your wedding venue. It’s a lovely place.
In a couple of words: not yet.
Metaprogramming is definitely on our radar, and we have had some internal discussions regarding it, but it’s not one of the top-priority items right now.
To be blunt, performance is much more important than you think, even when building a proof of concept. We used the PoC code for much longer than was initially intended, and had we thought about performance from the start we might’ve saved quite a bit of work!
Can you expand more on what you mean here? We currently have a work-in-progress library for binding to Postgres, but I have the feeling that isn’t quite what you’re getting at.
Luna is very much a general-purpose programming language! We’re working on developing both the language and the libraries ecosystem until you can use it for whatever you’d like.
While data-analysis is our focus at the moment, that isn’t due to any current limitation on Luna the language. We still have more we want to do to the language, but there is nothing stopping you from writing whatever you want in it now!
The language core has been completely re-written, almost from scratch, with performance as an explicit goal.
The only news I can give you at the moment is that it’s still definitely planned! We’re hoping to work on it once we finish our performance improvement and new GUI work.
We’ve been very careful to base the editor on web technologies, and browser-based Luna is definitely on the cards once we finish the new GUI!
We should be getting both our Mac and Windows developer certificates this week. I’m really sorry for the inconvenience - it should be fixed by the time of the next release.
Oh, I understand what you mean now. My mistake! It is all displayed on Canvas at this point, which does go through JavaScript. We’re actually moving to our own WebGL-based canvas (BaseGL) for performance.
Brilliant! That’s a really great set of pointers - we’ll take those on board!
To contextualise this, it used to take minutes rather than seconds to load, typecheck and compute this project.
Thanks for the feedback! We’ll give our README files a bit of a once-over and see if we can communicate more of the ‘wow’ factor.
Ara here! I’m one of the compiler engineers on Luna!
We’ve just released our 1.4 performance update at [0], and Luna is now immeasurably more quick!
I’ll keep an eye on this thread and answer questions where I can!
Unfortunately not! The graph in Luna isn’t an external visualisation of parts of the data flow, but an explicit alternate syntax for the Luna AST. It’s isomorphic to the textual syntax.
It would be possible, perhaps, to use some of the machinery for display to draw other pipelines, but I work on the compiler rather than Luna Studio, so perhaps I’m not the best person to say!
This has some beautiful and magical synchronicities in it.
I should add that something like FStar [0] combines the capabilities of automated theorem proving and a more manual-proof-based dependent type system like that in Idris.
It doesn’t have some of the power of Idris’ elaborator reflection, for example, but it can eliminate many long-winded manual proofs via the SMT solver.
That’s not strictly true. You can malloc an m*n sized array and then assign to another array the pointer to the head of each column, allowing you standard style indexing.
I have to appreciate the humour this shows. All in the name of progress, and it certainly made me laugh.
SpaceX has somehow managed to turn landing a booster from space into something almost mundane, but it bears remembering the failures that got them there.
This is a haunting read, but gripping at the same time. Thank you for posting it.