A bit tangential, but I really *really* appreciate them making this distinction, and wish more people did this. Way too many tools try to advertise themselves as all things for all people, catering to all use cases, and that helps nobody.
Vx – One Language, Every Chip (vxlang.org)
pdpi 2 hours ago
jack_h 31 minutes ago
I've actually created some experimental DSL embeddings around this idea before as I find it a fascinating area. Skimming through the Vx docs it seems like it is moving some of the abstract machine into the type system for greater flexibility.
png732 3 hours ago
Skwid 2 hours ago
yewenjie 2 hours ago
Cyan488 3 hours ago
Is the intent that applications developed with this are compiled for target hardware on a machine-specific basis?
e.g. I define a machine file for my i5 and GTX3080, and another machine file for my gnarly datacenter rack, and the compiler compiles specifically for each?
That way the same source file is "provable" for different hardware configurations without relying on a runtime to be identicallu implemented?
dev_dan_2 an hour ago
- "Most compilers hard-code a cost model. Vx reads one. A machine file describes the memory hierarchy and interconnect of a real part, and the compiler admits or rejects placements against it." I also designed it so that the target system is described by a single file that is picked up by the static analysis - cool!
- "Where data lives is part of its type" also doing that - when I got my project to an mvp state; I need to check out how vxlang does what it does: do they use a literal typesystem, or also compile checks outside of that? If its a type system, is it a dependent type system, or another flavor?
Yet another motivation to finally get my side project starting (forth-adjacent, many similar claims with regards to compile-time checks as vxlang; however, I still have to achieve that, while they already seem to have at least those and more in place; kudos to the vxlang team!)
IshKebab an hour ago
Muromec an hour ago
airstrike 36 minutes ago
NBJack 16 minutes ago
amelius 3 hours ago
Sounds like a great language for an AI to use then :)
api 3 hours ago
paufernandez an hour ago
AnimalMuppet 4 hours ago
dnautics 3 hours ago
treyd 2 hours ago
You do that by making the type system more sophisticated.
If you have a really important invariant that you really don't want to be violated due to run-time behavior/input, it's a huge benefit to have a compiler that can statically check that it actually can't be. That's one of the main benefits of having type systems, not just describing the shape of data structures in memory.
dnautics 2 hours ago
C is a bad language to do this with for various reasons, but as a simple example:
char* buf = malloc(SIZE);
free(buf);
free(buf);
There is absolutely no reason why static analysis should not be able to see what the problem is here.binary132 2 hours ago
0xdeafbeef an hour ago
How will you find such violations if opaque comes from so or some ffi, so compiler can't see through? you can't. It's heuristics. Sound type system is much stronger
kfsone an hour ago
``` ((void()(void) free)(buf); ((void()(void) free)(buf); ```
It's been my experience people invested in static analysis think of it like some wholly additive extension.
Compiler-independent static analysis is code applying rules. Someone has to write all the rules, align them with the language and the compiler. The user rarely reads the static analyzer's code or full rule definitions and is blissfully unaware of the full set of disconnects, inconsistences, and gaps between the coverage of the two.
They only notice divergence in the analysis when it generates a false-positive warning or error.
Static analysis adds compilation overhead. Sure, but I'd hazard that re-reading and in to some degree repeating the parsing/translation process that the compiler is going to do also introduces overhead.
There are some languages that demonstrate sta-by-compiler capabilities with heinous compile times, but it doesn't have to be that way. We can engineer better, but at some point it requires a price. Better comments, boilerplate of some kind or another, annotating intent over idiom.
A complex type system isn't ideal; with the right set of primitives you can achieve sophistication without complexity.
``` Freeable buf = malloc(SIZE); free(buf); // compiler error, you didn't check buf isn't valid. free(buf); // compiler error still if you fixed the above, free makes buf invalid. ```
"Making the compiler do STA makes it slow". I don't think that's proven one way or the other. There are examples both ways. "complex" type systems frequently have slow compilers, but if you look more closely that's usually because they're trying to compensate for the disconnect between organically emerged complexity in their under-designed type systems.
classified 2 hours ago
dnautics 2 hours ago
Do you not understand what static analysis is?
AnimalMuppet an hour ago
Now, sure, you could have some kind of annotations in the comments or something, and a static analyzer that checked those, and you could get that to check pretty much anything that can be checked statically. But at that point, it's not really part of the language, is it?
BatchJob 2 hours ago
ricardobeat 7 minutes ago
Please dedicate ten minutes of your time to reviewing your copy — so a person interested in your project walks away with understanding, not angry thoughts at three in the morning.
/s