I don't think it makes sense to ban them in a language with powerful enough checks, like dependent types. If you have two variables and one is typed "int 1-10" and the other is typed "int 1-5", and it fails at runtime if it doesn't fit in the destination range, why do you need to type something that says you really meant to assign one to the other? Just assign it.
I'm reading this as, "Many red boxes are blue circles." If the language allows implicit widening casts, it has implicit casts.
I don't think more powerful checks are necessary. It's just that the implicit conversions in C are a bit wild, and they result in unexpected behavior and surprise programmers, and from experience, making all casts explicit is not such a burden (except for stuff like char ptr -> const char ptr).
I think the fantasy here is simple... as much as we want to explore new ways to make safe programs with better type systems and runtime checks, there is still some design space near C which is safer but not really more complicated.
There seems to be an uncanny valley effect with C-like languages. The best you can do is have non-standard compiler extensions on top of ISO C.
We're not talking about making an entirely new language which is incompatible with C. You adopt a style guide, an accompanying static analysis tool, and maybe add some annotations to your source code. Your code is still C-compatible and you can still use the same compilers.
Static analysis of general C programs is quite difficult, and turning on an analyzer for an existing codebase typically results in obscene numbers of false positives. However, if you pair a static analyzer with a strict style guide which restricts the language, you can make the static analyzer much more powerful and useful.
This could be MISRA, it could be a formal verification system, or it could be something else entirely.
The problem is that people state things like "Java doesn't have implicit casts for correctness." But then it does have implicit casts, so now is there still correctness?
Another case is Haskell, where the wiki tells you:
> Conversion between numerical types in Haskell must be done explicitly. This is unlike many traditional languages (such as C or Java) that automatically coerce between numerical types.
But what this actually means is instead of `a = b` you do `a = fromInteger b`. This is obviously also an implicit cast, because Haskell has type inference. So again, you're not writing a proof that your conversion is correct. You're just writing a different, longer "yes I really mean to assign this" statement.
I am a bit too tired to engage with this kind of outright insanity. If you have a problem with what "people state", but not specifically with what I state or what has been stated in this conversation, then go have arguments with "people".
The idea that "Java has correctness" or "Java does not have correctness" does not make any sense. Java is a language, it's the programs that you write with it that are correct or incorrect.
> This is obviously also an implicit cast, because Haskell has type inference.
Incorrect, it is an explicit conversion. There is no such thing as a "cast" in Haskell, there are only functions which convert values of one type to values of another type. (well, in FFI code, there are functions which "cast" pointers and the like, but that's FFI.)
And yes, you're not writing a proof that the conversion is correct. This is... blindingly obvious, so I have no idea what kind of point you are trying to make. "Ordinary Haskell code is not formally verified" is not news.
Touchy! I am claiming the people who want always explicit casts have not actually used a system where they're all explicit much (because like in Java, some are still implicit) and would find it annoying if they did.
That could result in performance compromises, like using int arrays everywhere instead of smaller types. Which is fine for scalar values, but for arrays it wastes memory.
> Java is a language, it's the programs that you write with it that are correct or incorrect.
Surely this language feature is intended to promote correctness. What else are errors for?
> Incorrect, it is an explicit conversion.
But `a = (uint16_t)b` and `a = fromInteger b` aren't the same thing - in one you have to name the destination type and in the other you don't. One is more explicit than the other. Is one of them bad?
> "Ordinary Haskell code is not formally verified" is not news.
It is news to people who don't do numeric programming. "If it compiles it probably works" / "if it compiles it's probably correct" is a real thing said about the language said on this forum.
C clearly has issues (the implicit unsigned short->int promotion is totally wrong) but I think trapping on overflows at runtime would be a much better improvement than adding compile errors.
Yes. "Probably", as you said. "Probably" is much, much weaker than "formally verified".
Hey, I'm only human. You made some inane comments.
> I am claiming the people who want always explicit casts have not actually used a system where they're all explicit much (because like in Java, some are still implicit) and would find it annoying if they did.
That claim is trivially false... Go and Rust have explicit casts, and they're reasonably popular. For example, in Go,
var x int16
var y int32
x = y // ERROR!
x = int32(y) // ok
let x: i16 = 1;
let y: i32 = x; // ERROR!
let y = i32::from(x); // ok
let z = i16::from(y); // ERROR!
This is clearly false in practice, just look at extant Go and Rust code.
> But `a = (uint16_t)b` and `a = fromInteger b` aren't the same thing - in one you have to name the destination type and in the other you don't. One is more explicit than the other. Is one of them bad?
If that's a rhetorical question, just make your point.
The fromInteger function is an explicit conversion. The conversion is explicit, but the destination type isn't explicit. The source type isn't explicit either, but apparently that's okay... consider the C code:
int x = (int)y;
int x = (float->int)y;
> It is news to people who don't do numeric programming.
I'd say that it's blindingly obvious to people with a rudimentary understanding of programming.
> C clearly has issues (the implicit unsigned short->int promotion is totally wrong) but I think trapping on overflows at runtime would be a much better improvement than adding compile errors.
You can already -ftrapv if you like, but "trapping on overflow" is a contributing factor to the Ariane 5 disaster, and the lesson there is that trapping on overflow is not necessarily a safe default. The cost of runtime overflow checks is surprisingly large, too, which is why people so often turn it off in languages that support it out of the box (like C# and Ada). The mitigations for these problems will involve some combination of run-time checks, compile-time checks, and testing.
Can you link some examples that weren't obviously at least 50% tongue in cheek?