8 ms·

Counterexamples in Type Systems: programs that crash, segfault or explode (2021)

234 points by nequo 3y ago

paulddraper 3y ago
Still looking for the explosions...
- masklinn 3y ago
  That's because TorgueLang is TBA, but don't worry it'll be an explosions-based language.
epolanski 3y ago
This seems a super interesting read.
armchairhacker 3y ago
Fun fact: even theorem provers have counterexamples - Breaking Badfny: https://www.reddit.com/r/Coq/comments/x4d31y/breaking_badfny/ https://www.reddit.com/r/Coq/comments/x4d31y/breaking_badfny... - Falso (Coq): https://github.com/clarus/falso 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 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!)
- gnulinux 3y ago
  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 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 https://github.com/agda/agda/pull/5354
  - nerdponx 3y ago
    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.
  - Analemma_ 3y ago
    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?
    - HappyPanacea 3y ago
      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 https://ionathan.ch/2021/08/04/sized-types.html
- nickdrozd 3y ago
  > 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 https://hal.science/hal-04096390/document
  - CHY872 3y ago
    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.
  - IIAOPSW 3y ago
    I feel like getting stuck in an infinite loop is a more appropriate encoding of "undecidable"
- mananaysiempre 3y ago
  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.
mzs 3y ago
oh my, hadn't known about this yet - 8 years and still unsolved: https://github.com/rust-lang/rust/issues/25860 https://github.com/rust-lang/rust/issues/25860
- weinzierl 3y ago
  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?
  - nequo 3y ago
    Their issue tracker has a label for soundness holes: https://github.com/rust-lang/rust/labels/I-unsound https://github.com/rust-lang/rust/labels/I-unsound
  - Taywee 3y ago
    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 https://counterexamples.org/eventually-nothing.html
  - ReleaseCandidat 3y ago
    Don't know what's interesting for you, but this is definitly interesting: https://counterexamples.org/eventually-nothing.html https://counterexamples.org/eventually-nothing.html I've also found these https://counterexamples.org/nearly-universal.html https://counterexamples.org/nearly-universal.html https://counterexamples.org/selfishness.html https://counterexamples.org/selfishness.html
  - deleted 3y ago
    [deleted]
- zyedidia 3y ago
  I came across this issue in Rust recently: https://github.com/rust-lang/rust/issues/57893 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/ https://zyedidia.github.io/blog/posts/5-safe-transmute/.
Konohamaru 3y ago
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.
- jnwatson 3y ago
  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.
- nerdponx 3y ago
  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.
  - norir 3y ago
    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.
  - lmm 3y ago
    I've found two segfaults in a 10+ year Java (well, actually mostly Scala) career (both known JVM bugs). It's rare, but possible.
rob74 3y ago
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...
- avgcorrection 3y ago
  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.
  - DaiPlusPlus 3y ago
    > 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?
    - stonemetal12 3y ago
      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.
- mrkeen 3y ago
  > 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?
Spivak 3y ago
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.
- cryptonector 3y ago
  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".
  - Jtsummers 3y ago
    > 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.
    - cryptonector 3y ago
      I'm trying to understand what GP meant by "strong" here. TFA doesn't say anything about "strength" of typing.
eimrine 3y ago
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).
- Jtsummers 3y ago
  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.
  - shadowgovt 3y ago
    Interestingly, common lisp does allow one to write unsound programs intentionally. The `the` special operator (http://clhs.lisp.se/Body/s_the.htm#the 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.
    - tmtvl 3y ago
      Ah yes, good old (declaim (optimize (safety 0)))
    - kazinator 3y ago
      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.
- 3y ago
awinter-py 3y ago
ugh first time I touched a haskell codebase it was crashing in prod and nobody knew why real 'this never happens' energy
- kccqzy 3y ago
  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.
  - suntipa 3y ago
    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.
    - kccqzy 3y ago
      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.
      - suntipa 3y ago
        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.
kazinator 3y ago
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.
- less_less 3y ago
  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).
  - kazinator 3y ago
    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.
afc 3y ago
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).
- dtech 3y ago
  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.
- Jtsummers 3y ago
  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.
- z3t4 3y ago
  Dynamic type languages usually have a very strong type system - that makes it impossible to cause a type error.
- lmm 3y ago
  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.
shadowgovt 3y ago
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.
- staunton 3y ago
  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.
  - shadowgovt 3y ago
    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.
dvt 3y ago
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.
s_gourichon 3y ago
> 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.
dataangel 3y ago
I love this
kelnos 3y ago
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.
- blueberry87 3y ago
  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.
syngrog66 3y ago
interesting, because I once did some (relatively novel/rare) work on segfaults, and was literalky reviewing my old C code related to it today
Zondartul 3y ago
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.
jamestimmins 3y ago
"Counterexamples" seems like a massively underexplored area for teaching good software design. "How to design good software" is a huge question, but "what are some mistakes you've seen with tool X" seems like a great way to catalogue common errors that people make while learning. I'd love for a major framework/tool to poll its users and create an index of common design counterexamples. e.g. "common design mistakes with serializers, models, caching, etc". +1 if that resource included ways to refactor away from the bad design. So if the counterexample is "Querying the database directly from the controller functions", there could be a list of ways to refactor a codebase away from that design in pieces, and what to consider at each step (since some problems aren't worth the effort of fixing).
- chrisshroba 3y ago
  Whoa, wanted to drop a comment and thank you for that framing. This would be such a useful tool even for internal documentation. Thanks!

234 points by nequo 3y ago

paulddraper 3y ago

Still looking for the explosions...

masklinn 3y ago
That's because TorgueLang is TBA, but don't worry it'll be an explosions-based language.

epolanski 3y ago

This seems a super interesting read.

armchairhacker 3y ago

Fun fact: even theorem provers have counterexamples - Breaking Badfny: https://www.reddit.com/r/Coq/comments/x4d31y/breaking_badfny/ https://www.reddit.com/r/Coq/comments/x4d31y/breaking_badfny... - Falso (Coq): https://github.com/clarus/falso 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 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!)

gnulinux 3y ago
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 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 https://github.com/agda/agda/pull/5354
- nerdponx 3y ago
  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.
- Analemma_ 3y ago
  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?
  - HappyPanacea 3y ago
    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 https://ionathan.ch/2021/08/04/sized-types.html
nickdrozd 3y ago
> 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 https://hal.science/hal-04096390/document
- CHY872 3y ago
  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.
- IIAOPSW 3y ago
  I feel like getting stuck in an infinite loop is a more appropriate encoding of "undecidable"
mananaysiempre 3y ago
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.

mzs 3y ago

oh my, hadn't known about this yet - 8 years and still unsolved: https://github.com/rust-lang/rust/issues/25860 https://github.com/rust-lang/rust/issues/25860

weinzierl 3y ago
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?
- nequo 3y ago
  Their issue tracker has a label for soundness holes: https://github.com/rust-lang/rust/labels/I-unsound https://github.com/rust-lang/rust/labels/I-unsound
- Taywee 3y ago
  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 https://counterexamples.org/eventually-nothing.html
- ReleaseCandidat 3y ago
  Don't know what's interesting for you, but this is definitly interesting: https://counterexamples.org/eventually-nothing.html https://counterexamples.org/eventually-nothing.html I've also found these https://counterexamples.org/nearly-universal.html https://counterexamples.org/nearly-universal.html https://counterexamples.org/selfishness.html https://counterexamples.org/selfishness.html
- deleted 3y ago
  [deleted]
zyedidia 3y ago
I came across this issue in Rust recently: https://github.com/rust-lang/rust/issues/57893 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/ https://zyedidia.github.io/blog/posts/5-safe-transmute/.

Konohamaru 3y ago

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.

jnwatson 3y ago
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.
nerdponx 3y ago
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.
- norir 3y ago
  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.
- lmm 3y ago
  I've found two segfaults in a 10+ year Java (well, actually mostly Scala) career (both known JVM bugs). It's rare, but possible.

rob74 3y ago

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...

avgcorrection 3y ago
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.
- DaiPlusPlus 3y ago
  > 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?
  - stonemetal12 3y ago
    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.
mrkeen 3y ago
> 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?

Spivak 3y ago

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.

cryptonector 3y ago
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".
- Jtsummers 3y ago
  > 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.
  - cryptonector 3y ago
    I'm trying to understand what GP meant by "strong" here. TFA doesn't say anything about "strength" of typing.

eimrine 3y ago

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).

Jtsummers 3y ago
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.
- shadowgovt 3y ago
  Interestingly, common lisp does allow one to write unsound programs intentionally. The `the` special operator (http://clhs.lisp.se/Body/s_the.htm#the 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.
  - tmtvl 3y ago
    Ah yes, good old (declaim (optimize (safety 0)))
  - kazinator 3y ago
    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.
3y ago

awinter-py 3y ago

ugh first time I touched a haskell codebase it was crashing in prod and nobody knew why real 'this never happens' energy

kccqzy 3y ago
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.
- suntipa 3y ago
  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.
  - kccqzy 3y ago
    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.
    - suntipa 3y ago
      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.

kazinator 3y ago

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.

less_less 3y ago
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).
- kazinator 3y ago
  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.

afc 3y ago

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).

dtech 3y ago
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.
Jtsummers 3y ago
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.
z3t4 3y ago
Dynamic type languages usually have a very strong type system - that makes it impossible to cause a type error.
lmm 3y ago
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.

shadowgovt 3y ago

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.

staunton 3y ago
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.
- shadowgovt 3y ago
  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.

dvt 3y ago

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.

s_gourichon 3y ago

> 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.

dataangel 3y ago

I love this

kelnos 3y ago

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.

blueberry87 3y ago
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.

syngrog66 3y ago

interesting, because I once did some (relatively novel/rare) work on segfaults, and was literalky reviewing my old C code related to it today

Zondartul 3y ago

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.

jamestimmins 3y ago

"Counterexamples" seems like a massively underexplored area for teaching good software design. "How to design good software" is a huge question, but "what are some mistakes you've seen with tool X" seems like a great way to catalogue common errors that people make while learning. I'd love for a major framework/tool to poll its users and create an index of common design counterexamples. e.g. "common design mistakes with serializers, models, caching, etc". +1 if that resource included ways to refactor away from the bad design. So if the counterexample is "Querying the database directly from the controller functions", there could be a list of ways to refactor a codebase away from that design in pieces, and what to consider at each step (since some problems aren't worth the effort of fixing).

chrisshroba 3y ago
Whoa, wanted to drop a comment and thank you for that framing. This would be such a useful tool even for internal documentation. Thanks!