(You can also get the theorem prover itself to hang or crash; if you work with theorem provers often, you'll even do this unintentionally, many times!)
Not just simple counterexamples (i.e. programming "bugs"), some theorem provers have systematic bugs that were discovered later and required programming language change because people building it weren't sure how to fix it, mathematically speaking.
For example, in Agda, there are two ways to create coinductive types. The most liberal and useful one uses a technique called "Sized Types". Sized Types are types where you annotate each type with a compile type upperbound "size" which allows compiler to prove a given coinductive computation on this object will terminate. You can image a conductive list "List T i" where "i" is a "Size Type". Ultimately, the compiler implements this using a mix of lazy evaluation and bookkeeping upperbounds using natural numbers.
Originally, this was part of the "safe" subset of the language. Meaning, you can write Agda code using Sized Types, and Agda compiler claims the subset of the language you use is sound. This means you cannot prove inconsistencies. Here comes this "bug" which showed otherwise: https://github.com/agda/agda/issues/1201 Since 2015 Agda developers have been working on ways to mitigate this problem. Finding no such solution, they eventually decided in May 2021 to remove Sized Types from the "safe" subset of the language: https://github.com/agda/agda/pull/5354
It's probably worth distinguishing between "compiler bugs" and "fundamental theoretical problems". From what I've seen of Idris 2 development, sometimes what looks like the former turns out to be the latter. But what I find really cool is that the theoretical problems are not necessarily unsolvable, and there seems to be a steady stream of new theoretical results that find their way into compilers. So even if we are a very long way off from these languages gaining wide adoption, it's exciting to see that progress is in fact being made, even if it's slow.
This is not my area of expertise, but I clicked around those Agda bugs with some interest, and it seems like all those problems are stemming from the fact that they defined inf < inf. A couple people mentioned addressing the issue by getting rid of that, and others objected that it would cause more problems than it solved. What are those problems? Why is inf < inf?
This is also not my area of expertise, but considering they are using sized types to prove termination through well-foundness so they are probably suppose to be ordinals where we can have ω < ω+1 but for some reasons they decide to forgo to distinguish between everything larger than ω and denote it as inf.
> You can also get the theorem prover itself to hang or crash; if you work with theorem provers often, you'll even do this unintentionally, many times!
Proving something false is a grave sin for a prover. On the other hand, failing to prove something true is not only forgivable, but inevitable as per the incompleteness theorem. While ideally this failure would presented in terms of a nice error message, crashes are preferable to unsoundness. Crashes can even be deliberately induced as a defensive measure: https://hal.science/hal-04096390/document
It really depends on how automated the prover is, this is kind of like reinforcement learning optimising something unintentionally. Theorem prover bugs are problematic if relied upon, but most of the bugs folks cite are only usable in very strange circumstances, and most practitioners will not see their results invalidated by such a bug. E.g. iirc falso required a type with more than 256 variants. If you don’t have one of those, it won’t affect you!
Essentially, you fix the bug, re-run your hol or whatever, and hope your theorem is still true.
Obviously this only applies to bugs in the implementation as opposed to an unsound logic.
The tongue-in-cheek MOTD of the Agda IRC channel outright says “We last proved false at ...”.
Of course, Agda is somewhat unusual because they are kind of making up the (very strong) logical theory as they go along instead of having a fixed core logic they could dump proofs in for double-checking, like Coq. On the flip side, Agda actually makes for a halfway usable programming language—unlike Coq.
One thing that wasn't always clear to me: how many of these examples crash due to bugs in the compiler/verifier, and how many because the type system is actually unsound?
Sometimes it is mentioned; a Rust example and a Java example were fixed years ago. So it seems... a little unfair? Obviously all software has bugs; compilers are no exception. Examples where the type system itself is unsound, and can't be fixed without a redesign, are IMO the only interesting ones.
The point of this website isn't to mock software that has bugs - it's to show pitfalls that have been fallen into before, and could be fallen into again. If popular languages have encountered them in the past, and fixed them, why not document it? Helps people in the future. Sure, actual examples of pure unsoundness are more interesting, but creating unsoundness in what should be a sound system is also useful to implementers of these sorts of systems.
Looks like the requirements for a "type system" have increased since I last looked - according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc. And here was I thinking that every strongly typed language already has a type system (a more or less sound one, but a type system)? Ok, TBF they mention that they are using a "fairly narrow" (re)definition of the term...
From the specific perspective of the article, C++’s type system is uninteresting because it’s so trivially and fundamentally unsound. It’s easy to come up with a single line of C++ (eg. overflowing a signed int) that works as a counterexample. Languages whose type systems make stronger guarantees you have to make an effort to break.
A type system that allows undefined behavior is equivalent to a logic system that allows proving a falsehood, and ex falso quodlibet – from a falsehood you can prove anything.
There’s a difference between a type system and a type system that is sound.
> according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc.
Soundness is a technical term.
Things can get pretty weird if you allow memory corruption. Some languages say that certain things are Undefined Behavior. Imagine if a logician said the following:
- Here is my sound and complete logic
- By the way, some valid formulas will give you Undefined Behavior and I don’t care what happens in those cases
> Things can get pretty weird if you allow memory corruption. Some languages say that certain things are Undefined Behavior
UB in C allows for a lot more than just memory corruption though (c.f.: nasal demons). Also, what about alternatives to UB, such as requiring a compiler error and/or runtime fatal error?
If we consider a program a state machine, then a sound type system is one that rules out all operations for which the next state is undefined. So Null pointer dereference is sound in Java. The next state is well defined even if it is just throw a NPE. In C it is not, because there is no well defined next state.
> according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc.
I mean, you are hiding a lot of possibilities in "etc. etc.". So is the article, when it says "and the like" in the sentence you're referring to. The kinds of things that belong in this list are described as "generally some sort of safety property." That's a big big list of things. It's not a particularly strict or narrow definition of type system, IMO.
Take C. What does it mean when C's type system says a variable "x" has type "int"? Practically, it means the compiler knows how many bytes (let's say 4) to reserve on the stack for x. But what if the program, during the course of execution, tries to write an 8-byte piece of data to x? The language is broken if that can occur because the compiler was not justified in reserving only 4 bytes for x. So, part and parcel of C's type system is a global safety property: It promises, among many other things, that at runtime no assignment will ever occur to an int-typed variable unless the assignment payload is 4 bytes.
So this is exactly what the article is talking about. Local rules (e.g., "int x = y" is well-typed if y has type int) working together to guarantee a global safety property (no type mismatches can occur at runtime).
The failure of a type system to do this properly is a failure at being a type system. And indeed, since C has undefined behavior, it's type system falls apart immediately. It's just not even interesting to consider enumerating the ways it can be broken.
The type systems considered by this article are ostensibly supposed to not be broken the way C's is. That's what makes the counterexamples of this article so interesting.
You are conflating two different (but related) concepts. The requirements for type system to be a type system have not changed. Neither have the requirements for soundness. Most mainstream languages have tacitly accepted unsoundness for decades, but newer languages aim to have type systems with fewer and fewer unsound rough edges.
For example, I would consider Java to be a strongly-typed language, but it has quite a few unsoundness issues that can come up in regular, non-contrived code. Scala's type system is stronger and more full-featured, but it's not clear to me that it's significantly more sound. Rust, perhaps, has a (strong) type system with fewer soundness issues than both Java and Scala, but some issues do exist.
C and C++ have comparatively weak type systems (though C++'s is certainly stronger than C's), and their type systems have quite a few soundness issues, many of which that can be exposed via simple one-liners.
Also consider that soundness issues are not all created equal. I would much rather see a ClassCastException at runtime in a Java or Scala program, than see memory corruption (with possible security or data-integrity consequences) in a "valid" C/C++ program when I misuse memory designated as one type, as another. Certainly the best case would be a compiler that wouldn't allow it in the first place, but the Java/Scala example is nowhere near as bad as the C/C++ example.
> a type system only deserves that name if it prevents use-after-free errors
Or another way to look at it: if I tell you you're holding an Integer, and when you try to use it in addition, it explodes, was I really justified in telling you you were holding an Integer?
Depending on how you turn your head and squint, overflow is still well-defined: if I add a to b and it overflows to c, it still overflows to the same c every time. That means addition is sound in that architecture, it just has surprising consequences and some properties one would expect naively to hold for positive-integer arithmetic don't hold for the computer addition operation (such as c > a && c > b for all a > 0 and b > 0).
C/C++ (the standard) makes no claims about what happens if you overflow integers. The program might set all your variables in the whole program to zero if it likes. Of course the compiler vendors wouldn't do that but they're allowed to. That's what "undefined" means at least in C/C++.
If you require perfect, 100% soundness in all circumstances, then nothing is sound.
(Probably. We have things that we thought were sound, and later proved were not, so if you start with the list of things now that have no known holes, that's the upper limit of things that are possibly sound, modulo future holes.)
If you seriously try for perfection, you can sometimes get pretty close. But if you insist on perfection or nothing, you usually get nothing.
The problem is that in practice there is absolutely never any way to be 100% sure that the form is valid, the reasoning is correct, or that the premises are true. You can get pretty close to 100% but there might always be cases where you're not close enough "for all practical purposes".
We have cosmical background events which cannot be shielded 100% and also cannot be predicted. This (among thousands of other reasons) means that you can never prove 100% what any given program will do on a computer.
Indeed, it's impossible to prove absolutely any fact about a real physical system. You prove things about abstract mathematical objects. Such a proof may be useful in practice when the assumptions you made for the proof are satisfied to a sufficient degree in a sufficient number of cases. Whether this is the case or not is ultimately a matter of judgement (and data, for which you have to use judgement in collecting/interpreting it, and data, for which...)
By the way, the paper you're using to write proofs in mathematical logic is a physical system.
You are missing the point. This article isn't talking about a real physical system, we are talking about abstract mathematical objects. The study of type system is to formalize the type system so they can be studied using logic alone. That's why there is the matter with soundness, the topic of this thread. Soundness is abstract, not physical.
(The endless appeal to practicality and physicality is both tiring and irrelevant. Circles as a shape don't exist in the real world because you can't use physical objects to create a circle; at some point, perhaps at the level of atoms, the perfect smoothness of the ideal circle breaks down into discrete atoms. So circles don't exist. Does it bother me? No. Does it bother you? Evidently it does.)
In practice, there is such a thing as "more or less sound" and there are no perfect circles. None of these things bother me.
I responded to you because it seemed (no snark intended) that "more or less sound" things existing bothers you. The person who mentioned "more or less sound things" was referring to those things that exist in practice. The local discussion was (I thought) about type systems that exist in practice in the sense that a real practical C compiler has one. I think OP was justified in talking about this here, even if the article does not, because the theory exists at least in part to inform practice.
What does it even mean for a program to be well-typed if that program has "use-after-free errors, memory corruption etc. etc."? A program with C-style undefined behaviour could ipso facto fail with a type error on any given line.
> Welcome to Counterexamples in Type Systems, a compendium of horrible programs that crash, segfault or otherwise explode.
Many interesting quirks in type systems, surprising interference between separately innocuous type system features, but don't expect too many explosions.
Indeed, many of the tricks are years old (e.g., 2006) and are fixed in current versions of the language (or even are research paper involving experimental systems that were never released, e.g. Privacy violation in C# doesn't even use a syntax that released C# compilers use).
Mutable matching in Ocaml can be reproduced with ocaml 4.13, still, and cause a segfault.
I know we are talking about the Platonic ideal of a perfectly sound and logical type system where absolutely nothing ever goes wrong, or at least comparing existing systems to that seemingly impossible ideal but...
In the real world, if "proving False" summons dragons, then... just don't do that?
I don't think there will ever be a programming language where nothing can go wrong. Safe-er languages are good, but they are not an excuse to absolve oneself of the responsibility to check one's assumptions and react to problems that happen anyway.
It sounds dumb to say "just don't make errors" but even dumber to assume "errors cannot be made", so we always have to program defensively, even in "safe" languages.
Regarding Mutable Matching, that can be a documented feature. Programmers perpetrating mutation in pattern guards probably expect a certain behavior, like that patterns are evaluated from left to right, and so patterns after the mutation will capture its result. If that is documented and reliable, then changing it breaks valid code.
People who don't like it should avoid mutation.
I.e. the following requirement does not really compute: "I want to mutate inside a multi-case pattern, yet the pattern matching mechanism must itself refer to an immutable, private snapshot of the entire object, or behave as if that were the case."
The requirement for "soundness" there really doesn't make sense; the programmer has chosen to value mutation over soundness.
Soundness means that mutable matching doesn't break the type system. It's fine for the behavior to be well-defined and documented but unintuitive. But in a "safe" language, mutation during a pattern match shouldn't allow you to bitcast an int into a function and then call it (which will segfault or worse).
Yes; if one pattern matching case infers that some field of an object is a function, but that is mutated to int, another case cannot keep going with that assumption and generate code where the int is treated a function.
That would almost seem like a downstream compiler problem. If the pattern matching expander emits straightforward code, similar to what you would write by hand, then it would have to be the compiler doing the wrong thing there, like doing type inference without noticing that some location whose type was inferred was replaced by a differently typed object.
If pattern matching itself generates type hints for the compiler, then the fault could lie there.
Very interesting read. I had to chuckle a bit that they exclude C++ examples because the C++ type system doesn't even pretend to guarantee the behavior of the program is defined.
At least they don't pretend. On the other hand, they seriously try to define exactly which programs have defined bahavior and to define behavior for those. (I'm really not a fan of C++ but I'll grant them this good effort at least)
As of 2023, anyone whose language claims to guarantee behavior of all programs is either kidding themselves or will never have a user base to speak of for their language.
No disagreement, but there is such a thing as a language for which 99% of the programs you can write in it and compile successfully are sound... vs. C and C++, where you can create an unsound program with a handful of regular day-to-day operations on one line.
To my money (for c++ in particular), the ledge of soundness is so razor thin that I might as well assume it's not there.
I think this is an interesting doc, but the argument that global properties can be guaranteed by a type system is false, so there will trivially be counterexamples of type systems.
In fact, for any extensional type theory, we have the interesting result that type inhabitation is undecideable. Further, when looking at intersection types, there's also a theory saying they're undecideable, and many more edge cases which I can't remember. So the result is that we have a lot of "patching" in compilers or runtimes that try to fill some of these holes, but that's to be expected.
Why disqualify languages (like Python) simply because they execute type checks dynamically? You could as well try to find programs in these languages that crash (without containing any issues that the language's dynamic type system detects at any point, before the crash).
> It's intended as a resource for researchers, designers and implementors of static type systems, as well as programmers interested in how type systems fit together (or don't). [emphasis added]
Change the objective, and dynamic type systems would be appropriate.
What Python has literally isn't a type system; expressions in Python don't have (the thing that Python calls) types, only values do. So it wouldn't even be possible to do any of the stuff this page is doing in Python.
Because the definition of soundness is that if a program typechecks it does not crash at runtime. This is a collection of unsound programs that syill typecheck.
Since there is no difference in Python and other untyped languages between a potential typechecking stage and runtime the definition is meaningless for them.
Are there any reasons why searching Lisp word does not give any result? Possible reasons: its type system is uncrashable, its type system is as easy to crash as C program (I am too beginner to know which is true).
Probably for the same rationale they provided to exclude Python from examination:
> Python's type system: Dynamic languages like Python do local type checks to establish global safety properties. However, the type checks are not done purely on the program's source code before running it, but examine the actual runtime inputs as well.
Interestingly, common lisp does allow one to write unsound programs intentionally. The `the` special operator (http://clhs.lisp.se/Body/s_the.htm#the) declares that the form in the second position is of the type specified by the first position. You can imagine that this allows the runtime to crash early if the type is wrong, and you'd be right... But depending on the compiler you use, it also allows for the creation of unsound programs because you can set your flags such that the compiler uses the presence of `the` to make assumptions on the underlying types, letting the program evaluate faster by throwing out some runtime type checks.
declarations are promises to the compiler. You're saying you've off-loaded all the heavy type checking and done a better job of it yourself, and your results should be used. So whether things are sound depends on your personal type system, and the sanitization of inputs to the whole thing so that your assumptions are met.
Lisps are excluded from that page because they (mostly) don't play the dangerous game that the page is about.
The dangerous game is this:
1. Prove some things about the program graph.
2. Assume that your proof is correct, and translate the program accordingly (possibly with aggressive optimizations based on the proofs).
3. Remove all the proof artifacts from the program, such as types, and run the compiled code with no further safety net.*
The entire Counterexamples project speaks to the truth in Donald Knuths' famous quote:
"Beware of bugs in the above code; I have only proved it correct, not tried it."
--
* Even if there is a safety net, the selling point of the languages is that it's unnecessary. If the type system is supposed to catch something, but it's not caught, and results in a run-time error (safely caught and everything) that still demonstrates unsoundness. It's not behaving as advertized/hyped.
There's a big difference between crashing as in segfaults and crashing as in I should have handled an exception but I chose not to. I can trigger a crash by dividing by zero and not handling it in almost any language.
"Nobody knew why" could mean bad code, communication breakdown or a host of things. You can make code puzzling in any language.
Lazy evaluation also implies that Haskell programs can crash based on their input. That doesn't imply big input, simply that the input caused a space leak the author hadn't considered.
Try selling that to your boss who runs a mission-critical app.
I tested my Python app on a list with ten elements and it works fine. But in production I unexpectedly received a list with a million elements! It crashes! Or more likely, it repeatedly receives a short list but still runs out of memory due to a memory leak I hadn't considered.
Python doesn't prevent a bad software engineer from writing bad code. Try to sell that.
Lazy eval opens the floodgates for complex space leaks. Suppose you have a complicated algorithm that runs until it reaches mathematical convergence. In a lazy language like Haskell, those cycles of iteration/recursion can accumulate thunks and crash. Thunk accumulation and crashing can depend on input that you can't control or know in advance.
How do I know this? Because our big Haskell app died this way on live customer data and became a fiasco for my employer. We dumped Haskell and never looked back.
I don't doubt your experience, but in my experience judicious use of bang patterns and StrictData are enough to prevent those issues. It's no different from debugging and avoiding memory leaks in other languages. It just takes different skill sets that are more difficult to find.
Bang and StrictData are fine locally but things get enormously worse when that data flows into deeply-layered libraries that I don't own.
Then, I need to understand and modify the evaluation behavior of a deeply-layered external software stack, including its crazy type-level magic, all before a looming deadline.
Seriously, how is this good for my sanity or career?
The machinery is large-scale ML and discrete optimization over large/complex data structures, designed for a specific vertical industry. These algorithms run for hours and lazy eval was an engineering disaster. Our team had experienced Haskell developers who fought complicated space leaks night and day.
I find it funny that the author excludes Python's type system because python is strongly typed but the nature of runtime checking means you can't blow up your program.
That's not remotely a fair characterization of what TFA says about Python:
> This is intentionally a fairly narrow definition. Some examples of things that are not "type systems":
> Python's type system: Dynamic languages like Python do local type checks to establish global safety properties. However, the type checks are not done purely on the program's source code before running it, but examine the actual runtime inputs as well.
It does not say "python is strongly typed but [...]", not even "python is strongly typed". The words "strong", "strongly", and "strength" do not even appear. TFA says that Python being dynamic means it is not type-checked at compilation time -- that's practically the same as saying the opposite of "python is strongly typed" for most people's intended meaning of "strongly typed".
> TFA says that Python being dynamic means it is not type-checked at compilation time -- that's practically the same as saying the opposite of "python is strongly typed" for most people's intended meaning of "strongly typed".
Strong typing is a weak concept (pun intended). The most useful meaning is, roughly, no or little automatic type coercion (so a numeric tower might still be "strong", but coercing a string "1" into the number 1 is "weak"; `"1" + 1` => `"2"`). Anyone who uses "strong typing" as synonymous with "static typing" is making a very silly mistake.
I don't think there's a truly safe programming language. When I was an undergraduate talking to somebody at the C. S. department (I was not a C. S. student, but I talked with many C. S. students) somebody there said that the risk of segfaults in C and Java, when the program approaches hundreds of kloc, are about equal. It's only in small, ungeneralizable programs where Java's GC guarantees safety.
Some people know how to manage memory and others don't. If you know how to manage memory, even C is a safe language. If you don't, not even the most formally-verified garbage-collected language can save you.
That's one of those misguided deep sounding statements that are based in a fundamental lack of knowledge. What you, or this guy at the CS department, said is completely bullshit, evidenced by simple statistics of memory safety in languages. There is a reason many big companies are adopting Rust, and it's not just because "they feel like it" or they lack coders that "can program in C". E.g. take a look at: https://security.googleblog.com/2022/12/memory-safe-language...
Rust works because the Rust type system and development environment are tutors. They train up the developer like magic nannies until they learn how to correctly manage memory.
So the power of Rust comes from the the cooperation of the developer with the compiler and development environment willing to work through their severe instruction.
Developers in general unwilling to learn how to manage memory walk away from Rust based devteams.
Ok, there's still Java, Kotlin, Go and other memory safe languages in the sense of that they are statistically way less likely to have any memory related bugs compared to C, C++ or similar low-level no GC, no reference counting languages and thus the original argument of "good developers" not doing memory related bugs as well as "Java is as unsafe as C after a certain size" is utter bullshit.
At Google, that’s definitely not true. Our C code crashes way more often than our Java code.
Memory management is harder than just remembering to free. It requires a deep understanding of ownership, lifetimes, and threading. That is hard at scale unless it is built into the language.
> I don't think there's a truly safe programming language.
This is correct, technically, but you can achieve really high assurances of safety. "safe" is not a binary, but a spectrum.
The rest of the comment is patently false. It's actually close to the opposite of reality. The stricter the type system, the smaller the risk of unexpected behavior. Very very smart people who "know how to manage memory" use C and introduce memory errors very often. It's actually only in small, ungeneralizable programs where weaker type systems don't matter.
It's not the GC that guarantees safety. It's the encapsulation of every memory access inside a safe interface in the language's semantics. All the GC does is to make it possible to create the most popular interfaces over a finite memory.
And yeah, any bug on the interface or its implementation will lead to unsafe memory usage.
But anyway, no, if you make an interface where it's impossible to get memory corruption, you won't get memory corruption. It doesn't matter if the most inapt programmer on the world uses it. And the idea that people can manually manage memory on programs that are hundreds of megabytes large and created by many developers (or a single one at many different times) is about as wrong as the first part.
Oh jezz, anecdotes from people from academy, please.
>Some people know how to manage memory and others don't. If you know how to manage memory, even C is a safe language. If you don't, not even the most formally-verified garbage-collected language can save you.
Who knows how to manage memory then?
Windows engineers? Chromium engineers? Linux engineers?
all of them have history of failing at this, stop with this mindset.
I'm a firmware engineer. The languages I use most frequently for professional purposes are C and Rust. C is less "safe" than Rust, in the sense that a larger share of C code is susceptible to subtle footguns. Sure, if you poke at edge cases and fill your code with unsafe blocks, Rust will do bad things too. To me, this seems like a reasonable way of thinking about safety: it's all relative, and it's all context-dependent.
The conversation about language "safety" always leads to a bunch of goalpost-moving. Is a language with a safe type system still safe if its runtime is buggy? What if the OS/kernel has a bug? What if the CPU has a bug? How about anomalies in I/O hardware? Keep going down the rabbit hole, and you'll eventually reach the conclusion that all software is extremely fragile and could explode into a million pieces if a single cosmic ray goes the wrong way. Thinking about safety in an absolute sense isn't productive.
As an aside, your CS buddies told you a bunch of nonsense.
I've never encountered a segfault in Python that wasn't caused by interacting with C code. Is that claim even true about Java? unless it's a bug in the JVM itself, I'd be really really surprised to see an actual memory-related error arise from user-written code in any popular GCed language.
I luv C and have shipped tons of it in the past successfully enough but... to be frank C was, in effect, literally designed to cause/allow/enable segfaults. as a by-product of the "wild west" power of its & and * operators.
Can confirm I've only gotten the jvm to segfault when writing jni code -- never when writing vanilla java. To be generous to the OP though, perhaps the person who made the original comment was trying to write system code in java with lots of jni to access syscalls, or perhaps earlier versions of the jvm were less stable. The first jvm I ever used was 6, so I can't personally speak to earlier version.
Are you referring to the programming language, or the compiler and runtime environment necessary to execute the code? The Java Language Specification doesn't provide any strong guarantees of "safety". For example, it's certainly possible to write Java code with heap memory leaks or stack overflows. And I have run into multiple defects with the Oracle JVM that caused segfaults when executing certain code (although to Oracle's credit, their JVM is generally one of the highest quality and most reliable pieces of large platform software ever created).
Fun fact: even theorem provers have counterexamples
- Breaking Badfny: https://www.reddit.com/r/Coq/comments/x4d31y/breaking_badfny...
- Falso (Coq): https://github.com/clarus/falso
- Coq critical bugs (some of these mention potential ways to prove false): https://github.com/coq/coq/blob/master/dev/doc/critical-bugs
(You can also get the theorem prover itself to hang or crash; if you work with theorem provers often, you'll even do this unintentionally, many times!)
Not just simple counterexamples (i.e. programming "bugs"), some theorem provers have systematic bugs that were discovered later and required programming language change because people building it weren't sure how to fix it, mathematically speaking.
For example, in Agda, there are two ways to create coinductive types. The most liberal and useful one uses a technique called "Sized Types". Sized Types are types where you annotate each type with a compile type upperbound "size" which allows compiler to prove a given coinductive computation on this object will terminate. You can image a conductive list "List T i" where "i" is a "Size Type". Ultimately, the compiler implements this using a mix of lazy evaluation and bookkeeping upperbounds using natural numbers.
Originally, this was part of the "safe" subset of the language. Meaning, you can write Agda code using Sized Types, and Agda compiler claims the subset of the language you use is sound. This means you cannot prove inconsistencies. Here comes this "bug" which showed otherwise: https://github.com/agda/agda/issues/1201 Since 2015 Agda developers have been working on ways to mitigate this problem. Finding no such solution, they eventually decided in May 2021 to remove Sized Types from the "safe" subset of the language: https://github.com/agda/agda/pull/5354
It's probably worth distinguishing between "compiler bugs" and "fundamental theoretical problems". From what I've seen of Idris 2 development, sometimes what looks like the former turns out to be the latter. But what I find really cool is that the theoretical problems are not necessarily unsolvable, and there seems to be a steady stream of new theoretical results that find their way into compilers. So even if we are a very long way off from these languages gaining wide adoption, it's exciting to see that progress is in fact being made, even if it's slow.
This is not my area of expertise, but I clicked around those Agda bugs with some interest, and it seems like all those problems are stemming from the fact that they defined inf < inf. A couple people mentioned addressing the issue by getting rid of that, and others objected that it would cause more problems than it solved. What are those problems? Why is inf < inf?
This is also not my area of expertise, but considering they are using sized types to prove termination through well-foundness so they are probably suppose to be ordinals where we can have ω < ω+1 but for some reasons they decide to forgo to distinguish between everything larger than ω and denote it as inf.
Edit: I found an explanation https://ionathan.ch/2021/08/04/sized-types.html
> You can also get the theorem prover itself to hang or crash; if you work with theorem provers often, you'll even do this unintentionally, many times!
Proving something false is a grave sin for a prover. On the other hand, failing to prove something true is not only forgivable, but inevitable as per the incompleteness theorem. While ideally this failure would presented in terms of a nice error message, crashes are preferable to unsoundness. Crashes can even be deliberately induced as a defensive measure: https://hal.science/hal-04096390/document
It really depends on how automated the prover is, this is kind of like reinforcement learning optimising something unintentionally. Theorem prover bugs are problematic if relied upon, but most of the bugs folks cite are only usable in very strange circumstances, and most practitioners will not see their results invalidated by such a bug. E.g. iirc falso required a type with more than 256 variants. If you don’t have one of those, it won’t affect you!
Essentially, you fix the bug, re-run your hol or whatever, and hope your theorem is still true.
Obviously this only applies to bugs in the implementation as opposed to an unsound logic.
I feel like getting stuck in an infinite loop is a more appropriate encoding of "undecidable"
The tongue-in-cheek MOTD of the Agda IRC channel outright says “We last proved false at ...”.
Of course, Agda is somewhat unusual because they are kind of making up the (very strong) logical theory as they go along instead of having a fixed core logic they could dump proofs in for double-checking, like Coq. On the flip side, Agda actually makes for a halfway usable programming language—unlike Coq.
One thing that wasn't always clear to me: how many of these examples crash due to bugs in the compiler/verifier, and how many because the type system is actually unsound?
Sometimes it is mentioned; a Rust example and a Java example were fixed years ago. So it seems... a little unfair? Obviously all software has bugs; compilers are no exception. Examples where the type system itself is unsound, and can't be fixed without a redesign, are IMO the only interesting ones.
The point of this website isn't to mock software that has bugs - it's to show pitfalls that have been fallen into before, and could be fallen into again. If popular languages have encountered them in the past, and fixed them, why not document it? Helps people in the future. Sure, actual examples of pure unsoundness are more interesting, but creating unsoundness in what should be a sound system is also useful to implementers of these sorts of systems.
Looks like the requirements for a "type system" have increased since I last looked - according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc. And here was I thinking that every strongly typed language already has a type system (a more or less sound one, but a type system)? Ok, TBF they mention that they are using a "fairly narrow" (re)definition of the term...
From the specific perspective of the article, C++’s type system is uninteresting because it’s so trivially and fundamentally unsound. It’s easy to come up with a single line of C++ (eg. overflowing a signed int) that works as a counterexample. Languages whose type systems make stronger guarantees you have to make an effort to break.
A type system that allows undefined behavior is equivalent to a logic system that allows proving a falsehood, and ex falso quodlibet – from a falsehood you can prove anything.
There’s a difference between a type system and a type system that is sound.
> according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc.
Soundness is a technical term.
Things can get pretty weird if you allow memory corruption. Some languages say that certain things are Undefined Behavior. Imagine if a logician said the following:
- Here is my sound and complete logic
- By the way, some valid formulas will give you Undefined Behavior and I don’t care what happens in those cases
That would be pretty wild.
> Things can get pretty weird if you allow memory corruption. Some languages say that certain things are Undefined Behavior
UB in C allows for a lot more than just memory corruption though (c.f.: nasal demons). Also, what about alternatives to UB, such as requiring a compiler error and/or runtime fatal error?
If we consider a program a state machine, then a sound type system is one that rules out all operations for which the next state is undefined. So Null pointer dereference is sound in Java. The next state is well defined even if it is just throw a NPE. In C it is not, because there is no well defined next state.
> according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc.
I mean, you are hiding a lot of possibilities in "etc. etc.". So is the article, when it says "and the like" in the sentence you're referring to. The kinds of things that belong in this list are described as "generally some sort of safety property." That's a big big list of things. It's not a particularly strict or narrow definition of type system, IMO.
Take C. What does it mean when C's type system says a variable "x" has type "int"? Practically, it means the compiler knows how many bytes (let's say 4) to reserve on the stack for x. But what if the program, during the course of execution, tries to write an 8-byte piece of data to x? The language is broken if that can occur because the compiler was not justified in reserving only 4 bytes for x. So, part and parcel of C's type system is a global safety property: It promises, among many other things, that at runtime no assignment will ever occur to an int-typed variable unless the assignment payload is 4 bytes.
So this is exactly what the article is talking about. Local rules (e.g., "int x = y" is well-typed if y has type int) working together to guarantee a global safety property (no type mismatches can occur at runtime).
The failure of a type system to do this properly is a failure at being a type system. And indeed, since C has undefined behavior, it's type system falls apart immediately. It's just not even interesting to consider enumerating the ways it can be broken.
The type systems considered by this article are ostensibly supposed to not be broken the way C's is. That's what makes the counterexamples of this article so interesting.
You are conflating two different (but related) concepts. The requirements for type system to be a type system have not changed. Neither have the requirements for soundness. Most mainstream languages have tacitly accepted unsoundness for decades, but newer languages aim to have type systems with fewer and fewer unsound rough edges.
For example, I would consider Java to be a strongly-typed language, but it has quite a few unsoundness issues that can come up in regular, non-contrived code. Scala's type system is stronger and more full-featured, but it's not clear to me that it's significantly more sound. Rust, perhaps, has a (strong) type system with fewer soundness issues than both Java and Scala, but some issues do exist.
C and C++ have comparatively weak type systems (though C++'s is certainly stronger than C's), and their type systems have quite a few soundness issues, many of which that can be exposed via simple one-liners.
Also consider that soundness issues are not all created equal. I would much rather see a ClassCastException at runtime in a Java or Scala program, than see memory corruption (with possible security or data-integrity consequences) in a "valid" C/C++ program when I misuse memory designated as one type, as another. Certainly the best case would be a compiler that wouldn't allow it in the first place, but the Java/Scala example is nowhere near as bad as the C/C++ example.
> a type system only deserves that name if it prevents use-after-free errors
Or another way to look at it: if I tell you you're holding an Integer, and when you try to use it in addition, it explodes, was I really justified in telling you you were holding an Integer?
That's kind of a bad example because adding integers can overflow (in some languages).
Depending on how you turn your head and squint, overflow is still well-defined: if I add a to b and it overflows to c, it still overflows to the same c every time. That means addition is sound in that architecture, it just has surprising consequences and some properties one would expect naively to hold for positive-integer arithmetic don't hold for the computer addition operation (such as c > a && c > b for all a > 0 and b > 0).
C/C++ (the standard) makes no claims about what happens if you overflow integers. The program might set all your variables in the whole program to zero if it likes. Of course the compiler vendors wouldn't do that but they're allowed to. That's what "undefined" means at least in C/C++.
> C/C++ (the standard) makes no claims about what happens if you overflow integers.
It makes no claims on what happens when you overflow signed integers.
Unsigned integer wrapping is specified by section 6.2.5, paragraph 9 of the C standard.
> more or less sound
There isn't more or less sound. There's really only sound or not.
Then there's really only "not".
If you require perfect, 100% soundness in all circumstances, then nothing is sound.
(Probably. We have things that we thought were sound, and later proved were not, so if you start with the list of things now that have no known holes, that's the upper limit of things that are possibly sound, modulo future holes.)
If you seriously try for perfection, you can sometimes get pretty close. But if you insist on perfection or nothing, you usually get nothing.
>If you require perfect, 100% soundness in all circumstances, then nothing is sound.
Soundness in logic requires both valid form, and reasoning from true premises.
The problem is that in practice there is absolutely never any way to be 100% sure that the form is valid, the reasoning is correct, or that the premises are true. You can get pretty close to 100% but there might always be cases where you're not close enough "for all practical purposes".
We have cosmical background events which cannot be shielded 100% and also cannot be predicted. This (among thousands of other reasons) means that you can never prove 100% what any given program will do on a computer.
Indeed, it's impossible to prove absolutely any fact about a real physical system. You prove things about abstract mathematical objects. Such a proof may be useful in practice when the assumptions you made for the proof are satisfied to a sufficient degree in a sufficient number of cases. Whether this is the case or not is ultimately a matter of judgement (and data, for which you have to use judgement in collecting/interpreting it, and data, for which...)
By the way, the paper you're using to write proofs in mathematical logic is a physical system.
You are missing the point. This article isn't talking about a real physical system, we are talking about abstract mathematical objects. The study of type system is to formalize the type system so they can be studied using logic alone. That's why there is the matter with soundness, the topic of this thread. Soundness is abstract, not physical.
(The endless appeal to practicality and physicality is both tiring and irrelevant. Circles as a shape don't exist in the real world because you can't use physical objects to create a circle; at some point, perhaps at the level of atoms, the perfect smoothness of the ideal circle breaks down into discrete atoms. So circles don't exist. Does it bother me? No. Does it bother you? Evidently it does.)
In practice, there is such a thing as "more or less sound" and there are no perfect circles. None of these things bother me.
I responded to you because it seemed (no snark intended) that "more or less sound" things existing bothers you. The person who mentioned "more or less sound things" was referring to those things that exist in practice. The local discussion was (I thought) about type systems that exist in practice in the sense that a real practical C compiler has one. I think OP was justified in talking about this here, even if the article does not, because the theory exists at least in part to inform practice.
What does it even mean for a program to be well-typed if that program has "use-after-free errors, memory corruption etc. etc."? A program with C-style undefined behaviour could ipso facto fail with a type error on any given line.
oh my, hadn't known about this yet - 8 years and still unsolved: https://github.com/rust-lang/rust/issues/25860
I came across this issue in Rust recently: https://github.com/rust-lang/rust/issues/57893. I thought it was interesting since it lets you easily write transmute in safe Rust: https://zyedidia.github.io/blog/posts/5-safe-transmute/.
Me too, is there a list of soundness holes in Rust anywhere?
Also, if anyone has read the book, are there any interesting Rust counterexamples?
Their issue tracker has a label for soundness holes:
https://github.com/rust-lang/rust/labels/I-unsound
Don't know what's interesting for you, but this is definitly interesting: https://counterexamples.org/eventually-nothing.html I've also found these https://counterexamples.org/nearly-universal.html https://counterexamples.org/selfishness.html
Not a counterexample of the type system of Rust itself, but this one with LLVM following C and C++ definitions of "side-effects" is interesting: https://counterexamples.org/eventually-nothing.html
> Welcome to Counterexamples in Type Systems, a compendium of horrible programs that crash, segfault or otherwise explode.
Many interesting quirks in type systems, surprising interference between separately innocuous type system features, but don't expect too many explosions.
Indeed, many of the tricks are years old (e.g., 2006) and are fixed in current versions of the language (or even are research paper involving experimental systems that were never released, e.g. Privacy violation in C# doesn't even use a syntax that released C# compilers use).
Mutable matching in Ocaml can be reproduced with ocaml 4.13, still, and cause a segfault.
I know we are talking about the Platonic ideal of a perfectly sound and logical type system where absolutely nothing ever goes wrong, or at least comparing existing systems to that seemingly impossible ideal but... In the real world, if "proving False" summons dragons, then... just don't do that? I don't think there will ever be a programming language where nothing can go wrong. Safe-er languages are good, but they are not an excuse to absolve oneself of the responsibility to check one's assumptions and react to problems that happen anyway. It sounds dumb to say "just don't make errors" but even dumber to assume "errors cannot be made", so we always have to program defensively, even in "safe" languages.
Regarding Mutable Matching, that can be a documented feature. Programmers perpetrating mutation in pattern guards probably expect a certain behavior, like that patterns are evaluated from left to right, and so patterns after the mutation will capture its result. If that is documented and reliable, then changing it breaks valid code.
People who don't like it should avoid mutation.
I.e. the following requirement does not really compute: "I want to mutate inside a multi-case pattern, yet the pattern matching mechanism must itself refer to an immutable, private snapshot of the entire object, or behave as if that were the case."
The requirement for "soundness" there really doesn't make sense; the programmer has chosen to value mutation over soundness.
Soundness means that mutable matching doesn't break the type system. It's fine for the behavior to be well-defined and documented but unintuitive. But in a "safe" language, mutation during a pattern match shouldn't allow you to bitcast an int into a function and then call it (which will segfault or worse).
Yes; if one pattern matching case infers that some field of an object is a function, but that is mutated to int, another case cannot keep going with that assumption and generate code where the int is treated a function.
That would almost seem like a downstream compiler problem. If the pattern matching expander emits straightforward code, similar to what you would write by hand, then it would have to be the compiler doing the wrong thing there, like doing type inference without noticing that some location whose type was inferred was replaced by a differently typed object.
If pattern matching itself generates type hints for the compiler, then the fault could lie there.
Very interesting read. I had to chuckle a bit that they exclude C++ examples because the C++ type system doesn't even pretend to guarantee the behavior of the program is defined.
At least they don't pretend. On the other hand, they seriously try to define exactly which programs have defined bahavior and to define behavior for those. (I'm really not a fan of C++ but I'll grant them this good effort at least)
As of 2023, anyone whose language claims to guarantee behavior of all programs is either kidding themselves or will never have a user base to speak of for their language.
No disagreement, but there is such a thing as a language for which 99% of the programs you can write in it and compile successfully are sound... vs. C and C++, where you can create an unsound program with a handful of regular day-to-day operations on one line.
To my money (for c++ in particular), the ledge of soundness is so razor thin that I might as well assume it's not there.
I think this is an interesting doc, but the argument that global properties can be guaranteed by a type system is false, so there will trivially be counterexamples of type systems.
In fact, for any extensional type theory, we have the interesting result that type inhabitation is undecideable. Further, when looking at intersection types, there's also a theory saying they're undecideable, and many more edge cases which I can't remember. So the result is that we have a lot of "patching" in compilers or runtimes that try to fill some of these holes, but that's to be expected.
Why disqualify languages (like Python) simply because they execute type checks dynamically? You could as well try to find programs in these languages that crash (without containing any issues that the language's dynamic type system detects at any point, before the crash).
Because it isn't appropriate to their objective:
> It's intended as a resource for researchers, designers and implementors of static type systems, as well as programmers interested in how type systems fit together (or don't). [emphasis added]
Change the objective, and dynamic type systems would be appropriate.
What Python has literally isn't a type system; expressions in Python don't have (the thing that Python calls) types, only values do. So it wouldn't even be possible to do any of the stuff this page is doing in Python.
Because the definition of soundness is that if a program typechecks it does not crash at runtime. This is a collection of unsound programs that syill typecheck.
Since there is no difference in Python and other untyped languages between a potential typechecking stage and runtime the definition is meaningless for them.
Dynamic type languages usually have a very strong type system - that makes it impossible to cause a type error.
Are there any reasons why searching Lisp word does not give any result? Possible reasons: its type system is uncrashable, its type system is as easy to crash as C program (I am too beginner to know which is true).
Probably for the same rationale they provided to exclude Python from examination:
> Python's type system: Dynamic languages like Python do local type checks to establish global safety properties. However, the type checks are not done purely on the program's source code before running it, but examine the actual runtime inputs as well.
Interestingly, common lisp does allow one to write unsound programs intentionally. The `the` special operator (http://clhs.lisp.se/Body/s_the.htm#the) declares that the form in the second position is of the type specified by the first position. You can imagine that this allows the runtime to crash early if the type is wrong, and you'd be right... But depending on the compiler you use, it also allows for the creation of unsound programs because you can set your flags such that the compiler uses the presence of `the` to make assumptions on the underlying types, letting the program evaluate faster by throwing out some runtime type checks.
declarations are promises to the compiler. You're saying you've off-loaded all the heavy type checking and done a better job of it yourself, and your results should be used. So whether things are sound depends on your personal type system, and the sanitization of inputs to the whole thing so that your assumptions are met.
Ah yes, good old
Lisps are excluded from that page because they (mostly) don't play the dangerous game that the page is about.
The dangerous game is this:
1. Prove some things about the program graph.
2. Assume that your proof is correct, and translate the program accordingly (possibly with aggressive optimizations based on the proofs).
3. Remove all the proof artifacts from the program, such as types, and run the compiled code with no further safety net.*
The entire Counterexamples project speaks to the truth in Donald Knuths' famous quote:
"Beware of bugs in the above code; I have only proved it correct, not tried it."
--
* Even if there is a safety net, the selling point of the languages is that it's unnecessary. If the type system is supposed to catch something, but it's not caught, and results in a run-time error (safely caught and everything) that still demonstrates unsoundness. It's not behaving as advertized/hyped.
interesting, because I once did some (relatively novel/rare) work on segfaults, and was literalky reviewing my old C code related to it today
This seems a super interesting read.
I love this
Still looking for the explosions...
That's because TorgueLang is TBA, but don't worry it'll be an explosions-based language.
ugh first time I touched a haskell codebase it was crashing in prod and nobody knew why
real 'this never happens' energy
There's a big difference between crashing as in segfaults and crashing as in I should have handled an exception but I chose not to. I can trigger a crash by dividing by zero and not handling it in almost any language.
"Nobody knew why" could mean bad code, communication breakdown or a host of things. You can make code puzzling in any language.
Lazy evaluation also implies that Haskell programs can crash based on their input. That doesn't imply big input, simply that the input caused a space leak the author hadn't considered.
Try selling that to your boss who runs a mission-critical app.
So?
I tested my Python app on a list with ten elements and it works fine. But in production I unexpectedly received a list with a million elements! It crashes! Or more likely, it repeatedly receives a short list but still runs out of memory due to a memory leak I hadn't considered.
Python doesn't prevent a bad software engineer from writing bad code. Try to sell that.
Lazy eval opens the floodgates for complex space leaks. Suppose you have a complicated algorithm that runs until it reaches mathematical convergence. In a lazy language like Haskell, those cycles of iteration/recursion can accumulate thunks and crash. Thunk accumulation and crashing can depend on input that you can't control or know in advance.
How do I know this? Because our big Haskell app died this way on live customer data and became a fiasco for my employer. We dumped Haskell and never looked back.
I don't doubt your experience, but in my experience judicious use of bang patterns and StrictData are enough to prevent those issues. It's no different from debugging and avoiding memory leaks in other languages. It just takes different skill sets that are more difficult to find.
Bang and StrictData are fine locally but things get enormously worse when that data flows into deeply-layered libraries that I don't own.
Then, I need to understand and modify the evaluation behavior of a deeply-layered external software stack, including its crazy type-level magic, all before a looming deadline.
Seriously, how is this good for my sanity or career?
What’s your product if you don't mind sharing? Curious.
The machinery is large-scale ML and discrete optimization over large/complex data structures, designed for a specific vertical industry. These algorithms run for hours and lazy eval was an engineering disaster. Our team had experienced Haskell developers who fought complicated space leaks night and day.
0/10 would not recommend.
And what are you using now?
The heavy numerical work is in julia, python, R, and a little custom c++ where necessary. Team productivity has gone way up.
yes but haskell code is inherently puzzling and you are supposed to get safety in exchange
What turned out to be the reason for the crashes in production?
unknown
Then it's a stretch to conclude that the problem was Haskell!
I find it funny that the author excludes Python's type system because python is strongly typed but the nature of runtime checking means you can't blow up your program.
That's not remotely a fair characterization of what TFA says about Python:
> This is intentionally a fairly narrow definition. Some examples of things that are not "type systems":
> Python's type system: Dynamic languages like Python do local type checks to establish global safety properties. However, the type checks are not done purely on the program's source code before running it, but examine the actual runtime inputs as well.
It does not say "python is strongly typed but [...]", not even "python is strongly typed". The words "strong", "strongly", and "strength" do not even appear. TFA says that Python being dynamic means it is not type-checked at compilation time -- that's practically the same as saying the opposite of "python is strongly typed" for most people's intended meaning of "strongly typed".
> TFA says that Python being dynamic means it is not type-checked at compilation time -- that's practically the same as saying the opposite of "python is strongly typed" for most people's intended meaning of "strongly typed".
Strong typing is a weak concept (pun intended). The most useful meaning is, roughly, no or little automatic type coercion (so a numeric tower might still be "strong", but coercing a string "1" into the number 1 is "weak"; `"1" + 1` => `"2"`). Anyone who uses "strong typing" as synonymous with "static typing" is making a very silly mistake.
I'm trying to understand what GP meant by "strong" here. TFA doesn't say anything about "strength" of typing.
I don't think there's a truly safe programming language. When I was an undergraduate talking to somebody at the C. S. department (I was not a C. S. student, but I talked with many C. S. students) somebody there said that the risk of segfaults in C and Java, when the program approaches hundreds of kloc, are about equal. It's only in small, ungeneralizable programs where Java's GC guarantees safety.
Some people know how to manage memory and others don't. If you know how to manage memory, even C is a safe language. If you don't, not even the most formally-verified garbage-collected language can save you.
That's one of those misguided deep sounding statements that are based in a fundamental lack of knowledge. What you, or this guy at the CS department, said is completely bullshit, evidenced by simple statistics of memory safety in languages. There is a reason many big companies are adopting Rust, and it's not just because "they feel like it" or they lack coders that "can program in C". E.g. take a look at: https://security.googleblog.com/2022/12/memory-safe-language...
Rust works because the Rust type system and development environment are tutors. They train up the developer like magic nannies until they learn how to correctly manage memory.
So the power of Rust comes from the the cooperation of the developer with the compiler and development environment willing to work through their severe instruction.
Developers in general unwilling to learn how to manage memory walk away from Rust based devteams.
Ok, there's still Java, Kotlin, Go and other memory safe languages in the sense of that they are statistically way less likely to have any memory related bugs compared to C, C++ or similar low-level no GC, no reference counting languages and thus the original argument of "good developers" not doing memory related bugs as well as "Java is as unsafe as C after a certain size" is utter bullshit.
At Google, that’s definitely not true. Our C code crashes way more often than our Java code.
Memory management is harder than just remembering to free. It requires a deep understanding of ownership, lifetimes, and threading. That is hard at scale unless it is built into the language.
> I don't think there's a truly safe programming language.
This is correct, technically, but you can achieve really high assurances of safety. "safe" is not a binary, but a spectrum.
The rest of the comment is patently false. It's actually close to the opposite of reality. The stricter the type system, the smaller the risk of unexpected behavior. Very very smart people who "know how to manage memory" use C and introduce memory errors very often. It's actually only in small, ungeneralizable programs where weaker type systems don't matter.
It's not the GC that guarantees safety. It's the encapsulation of every memory access inside a safe interface in the language's semantics. All the GC does is to make it possible to create the most popular interfaces over a finite memory.
And yeah, any bug on the interface or its implementation will lead to unsafe memory usage.
But anyway, no, if you make an interface where it's impossible to get memory corruption, you won't get memory corruption. It doesn't matter if the most inapt programmer on the world uses it. And the idea that people can manually manage memory on programs that are hundreds of megabytes large and created by many developers (or a single one at many different times) is about as wrong as the first part.
Oh jezz, anecdotes from people from academy, please.
>Some people know how to manage memory and others don't. If you know how to manage memory, even C is a safe language. If you don't, not even the most formally-verified garbage-collected language can save you.
Who knows how to manage memory then?
Windows engineers? Chromium engineers? Linux engineers?
all of them have history of failing at this, stop with this mindset.
I'm a firmware engineer. The languages I use most frequently for professional purposes are C and Rust. C is less "safe" than Rust, in the sense that a larger share of C code is susceptible to subtle footguns. Sure, if you poke at edge cases and fill your code with unsafe blocks, Rust will do bad things too. To me, this seems like a reasonable way of thinking about safety: it's all relative, and it's all context-dependent.
The conversation about language "safety" always leads to a bunch of goalpost-moving. Is a language with a safe type system still safe if its runtime is buggy? What if the OS/kernel has a bug? What if the CPU has a bug? How about anomalies in I/O hardware? Keep going down the rabbit hole, and you'll eventually reach the conclusion that all software is extremely fragile and could explode into a million pieces if a single cosmic ray goes the wrong way. Thinking about safety in an absolute sense isn't productive.
As an aside, your CS buddies told you a bunch of nonsense.
I've never encountered a segfault in Python that wasn't caused by interacting with C code. Is that claim even true about Java? unless it's a bug in the JVM itself, I'd be really really surprised to see an actual memory-related error arise from user-written code in any popular GCed language.
I luv C and have shipped tons of it in the past successfully enough but... to be frank C was, in effect, literally designed to cause/allow/enable segfaults. as a by-product of the "wild west" power of its & and * operators.
Can confirm I've only gotten the jvm to segfault when writing jni code -- never when writing vanilla java. To be generous to the OP though, perhaps the person who made the original comment was trying to write system code in java with lots of jni to access syscalls, or perhaps earlier versions of the jvm were less stable. The first jvm I ever used was 6, so I can't personally speak to earlier version.
I've found two segfaults in a 10+ year Java (well, actually mostly Scala) career (both known JVM bugs). It's rare, but possible.
Are you referring to the programming language, or the compiler and runtime environment necessary to execute the code? The Java Language Specification doesn't provide any strong guarantees of "safety". For example, it's certainly possible to write Java code with heap memory leaks or stack overflows. And I have run into multiple defects with the Oracle JVM that caused segfaults when executing certain code (although to Oracle's credit, their JVM is generally one of the highest quality and most reliable pieces of large platform software ever created).