LightMachine

3 ms·

1.
by LightMachine 8d ago
no, that's a good question. half of the point of HVM is to be an incredibly fast evaluator, in the "raw speed" sense. the other is to be an incredibly fast evaluator, in the "asymptotical" sense. in the first sense,
2.
by LightMachine 8d ago
You just vaguely called the language "worse" without bringing a single concrete point. I can't defend my design choices without knowing what you don't like about it
3.
by LightMachine 8d ago
I don't know either :( I'm not a celebrity and I don't like celebrities
4.
by LightMachine 8d ago
I think people are genuinely bitter about it, that's usually how my projects are received
5.
by LightMachine 8d ago
(author here) Bend1 indeed has no significant active userbase I don't think that means it was "unsuccessful" in the sense you imply, though, because the project was never meant to be used in production. It was there to displa
6.
by LightMachine 8d ago
It will, there is just too much to do! It is a programming language. With a consistent, non-standard proof system. That compiles to GPUs. We're a small team. Please be patient
7.
by LightMachine 8d ago
Victor here. I haven't "worked" on Formality. I've founded it. Designed every part of it. Before LLMs! sighs Here's my response to this ridiculous accusation: https://news.ycombinator.com/item?id=4
8.
by LightMachine 8d ago
Note that using linked lists for strings is actually more "parallel friendly" because you can take the head/tail and spread it around 16k GPU cores in O(1), unlike in Haskell, unlike arrays, which require a linear copy, becom
9.
by LightMachine 8d ago
1. LLM cost is inexpensive compared to the cost of a bug, and you can use tools to automate the proof-work, as you said so yourself. 2. Why would it? The AI shouldn't load already completed proofs, only their type signatures (which are
10.
by LightMachine 8d ago
The history is back...
11.
by LightMachine 8d ago
What about it isn't working for you?
12.
by LightMachine 8d ago
So are Haskell's, since 20 years ago, with no options for years? We will introducing binary buffers eventually. The project is new...
13.
by LightMachine 8d ago
"The developer has built an entire language around a field seemingly without realising that said field exists." That is incredibly funny. Here's a talk about formal verification I made 7 years ago @ DevCon: https:/&#x2F
14.
by LightMachine 8d ago
yeah that makes sense, thanks for the feedbacks!
15.
by LightMachine 8d ago
commit history is back now!
16.
by LightMachine 8d ago
the entire language is based on linear types! it says so in the GUIDE yes
17.
by LightMachine 8d ago
Ty! Commit history is back now
18.
by LightMachine 8d ago
Commit history is back!
19.
by LightMachine 8d ago
Commit history is back!
20.
by LightMachine 8d ago
Commit history is back!
21.
by LightMachine 8d ago
Commit history is back!
22.
by LightMachine 8d ago
1. I do, but probably not in the current version, since I believe these proofs probably need full closure cloning to be ergonomic. 2. You can express anything actually, because you can clone data, just not functions. So, anything you could
23.
by LightMachine 8d ago
The project got a lot of attention at launch, but it wasn't really ready to be used back then. There were too many limitations, like u24 numbers (yes), 2 GB memory limit, pervasive strictness (if-then-else executed both branches). It w
24.
by LightMachine 8d ago
I honestly had no idea people would be so upset about commit history. I just wanted to avoid leaking sensitive info, that's all. I'm running through the commits to ensure nothing personal leaks and I plan on putting the history ba
25.
by LightMachine 8d ago
should I read this as "I wish I could find a guy like you" :')
26.
by LightMachine 8d ago
good question we'll try
27.
by LightMachine 8d ago
Thank you!! Currently, parallelism works in any multi-core CPU, and in Apple M-series and NVIDIA GPUs.
28.
by LightMachine 8d ago
fixed ty
29.
by LightMachine 8d ago
Ohhh. Ok. I see the confusion. That's bad syntax then. The 'a' parameter is not the type of the elements. 'A' is the type of the elements. 'a' is just the "quantity of the type of the type of the elem
30.
by LightMachine 8d ago
2 isn't a big claim though, I think anyone developing Lean or Agda would agree these would be much faster with zero inference, unification or search? They'd just complain the language would become unergonomic, and that's true

More ›