I haven't played with it at all, but the writeup looks promising. Moving a bunch of things into the type system and out of runtime crashes is one of the ways we make progress.
I think this is wrong. Type systems should be simpler, and you should design it so that your language is easily and correctly statically checked. Not all invariants necessarily have to be verified at the same cadence (compile time)
> you should design it so that your language is easily and correctly statically checked.
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.
uintptr_t x = opaque((uintptr_t)p);
free((void *)x);
free(p);
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
I mean you can annotate it if you want. Just tell the analyzer in a separate file, get the variable at this line on this file has these guarantees.
You could even annotate dependencies that didn't use your static analyzer. You could track custom invariants that your language designer didn't put in the type system.
Which is why every library that wraps C APIs provides safe wrappers that express the implicit expectations within Rust's type system. Yes the low-level calls are unsafe, of course they are, but then we expose them with a safe interface that consumers actually use.
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.
Can't is a strong word. You could 100% put it in the compiler. Yet you don't (for the reasonable reasons you give). The line between compiler static analysis and non-compiler static analysis is a design decision. "defeating the point" is a subjective and pragmatic decision, not one rooted in safety absolutism.
We understand that static analysis is often less bulletproof than a compiler's type system. It doesn't always catch everything. If it does, it often says "may", and then you have to sort out the false positives from the real problems, and there can be a lot of them.
And if you don't take every problem seriously, and do a full investigation, then you are risking a real problem that you don't fix, which can turn into... a runtime crash.
But what does static analysis work on? The source code. If it's not in the source code, the static analyzer can't check it. So if you want to check something, even with a static analyzer, then you need some way to talk about that thing in the source code, which means it has to be part of the source language.
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?
AnimalMuppet · · focus · HN ↗
dnautics · · focus · HN ↗
treyd · · focus · HN ↗
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 · · focus · HN ↗
C is a bad language to do this with for various reasons, but as a simple example:
There is absolutely no reason why static analysis should not be able to see what the problem is here.binary132 · · focus · HN ↗
0xdeafbeef · · focus · HN ↗
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
dnautics · · focus · HN ↗
Christ. Even rust makes ffi unsafe.
I mean you can annotate it if you want. Just tell the analyzer in a separate file, get the variable at this line on this file has these guarantees.
You could even annotate dependencies that didn't use your static analyzer. You could track custom invariants that your language designer didn't put in the type system.
treyd · · focus · HN ↗
Which is why every library that wraps C APIs provides safe wrappers that express the implicit expectations within Rust's type system. Yes the low-level calls are unsafe, of course they are, but then we expose them with a safe interface that consumers actually use.
kfsone · · focus · HN ↗
``` ((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.
dnautics · · focus · HN ↗
steveklabnik · · focus · HN ↗
The compiler could interpret all unsafe via it but then it would be very slow, defeating the point.
dnautics · · focus · HN ↗
Can't is a strong word. You could 100% put it in the compiler. Yet you don't (for the reasonable reasons you give). The line between compiler static analysis and non-compiler static analysis is a design decision. "defeating the point" is a subjective and pragmatic decision, not one rooted in safety absolutism.
imtringued · · focus · HN ↗
buf_create(SIZE)
and
buf_destroy(buf)
now the compiler has to infer that buf_create creates a lifetime and buf_destroy destroys it.
we're back to Rust's Box.
dnautics · · focus · HN ↗
classified · · focus · HN ↗
dnautics · · focus · HN ↗
Do you not understand what static analysis is?
[deleted] · · focus · HN ↗
[deleted]
AnimalMuppet · · focus · HN ↗
And if you don't take every problem seriously, and do a full investigation, then you are risking a real problem that you don't fix, which can turn into... a runtime crash.
dnautics · · focus · HN ↗
AnimalMuppet · · focus · HN ↗
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?
dnautics · · focus · HN ↗