[HN Gopher] Counterexamples in Type Systems: programs that crash...
___________________________________________________________________
Counterexamples in Type Systems: programs that crash, segfault or
explode (2021)
Author : nequo
Score : 175 points
Date : 2023-06-06 14:51 UTC (8 hours ago)
(HTM) web link (counterexamples.org)
(TXT) w3m dump (counterexamples.org)
| epolanski wrote:
| This seems a super interesting read.
| dvt wrote:
| 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.
| eimrine wrote:
| 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 wrote:
| 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 wrote:
| 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.
| tmtvl wrote:
| Ah yes, good old (declaim (optimize (safety
| 0)))
| mzs wrote:
| oh my, hadn't known about this yet - 8 years and still unsolved:
| https://github.com/rust-lang/rust/issues/25860
| weinzierl wrote:
| 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 wrote:
| Their issue tracker has a label for soundness holes:
|
| https://github.com/rust-lang/rust/labels/I-unsound
| Taywee wrote:
| 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
| [deleted]
| ReleaseCandidat wrote:
| 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
| dataangel wrote:
| I love this
| afc wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| Dynamic type languages usually have a very strong type system -
| that makes it impossible to cause a type error.
| lmm wrote:
| 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.
| kelnos wrote:
| 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 wrote:
| 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.
| awinter-py wrote:
| ugh first time I touched a haskell codebase it was crashing in
| prod and nobody knew why
|
| real 'this never happens' energy
| kccqzy wrote:
| 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 wrote:
| 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.
| awinter-py wrote:
| yes but haskell code is inherently puzzling and you are
| supposed to get safety in exchange
| nequo wrote:
| What turned out to be the reason for the crashes in
| production?
| awinter-py wrote:
| unknown
| Konohamaru wrote:
| 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.
| ThereIsNoWorry wrote:
| 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...
| Konohamaru wrote:
| 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.
| ThereIsNoWorry wrote:
| 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.
| Taywee wrote:
| > 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.
| ryukoposting wrote:
| 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.
| jnwatson wrote:
| 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.
| marcosdumay wrote:
| 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.
| nerdponx wrote:
| 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 wrote:
| 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 wrote:
| I've found two segfaults in a 10+ year Java (well, actually
| mostly Scala) career (both known JVM bugs). It's rare, but
| possible.
| nradov wrote:
| 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).
| tester756 wrote:
| 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.
| s_gourichon wrote:
| > 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.
| kazinator wrote:
| 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 wrote:
| 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 wrote:
| 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.
| rob74 wrote:
| 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...
| cvoss wrote:
| > 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.
| avgcorrection wrote:
| 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 wrote:
| > 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 wrote:
| 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 wrote:
| > 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?
| rwmj wrote:
| That's kind of a bad example because adding integers can
| overflow (in some languages).
| shadowgovt wrote:
| 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).
| Sharlin wrote:
| 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.
| kelnos wrote:
| 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.
| lmm wrote:
| 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.
| kccqzy wrote:
| > more or less sound
|
| There isn't more or less sound. There's really only sound or
| not.
| AnimalMuppet wrote:
| 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.
| salawat wrote:
| >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_.
| staunton wrote:
| 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 ".
| staunton wrote:
| 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.
| kccqzy wrote:
| 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.)
| Spivak wrote:
| 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 wrote:
| 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 wrote:
| > 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 wrote:
| I'm trying to understand what GP meant by "strong" here.
| TFA doesn't say anything about "strength" of typing.
| paulddraper wrote:
| Still looking for the explosions...
| masklinn wrote:
| That's because TorgueLang is TBA, but don't worry it'll be an
| explosions-based language.
| armchairhacker wrote:
| 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!)
| gnulinux wrote:
| 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
| nerdponx wrote:
| 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_ wrote:
| 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 wrote:
| 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 o < o+1 but for some reasons they decide to
| forgo to distinguish between everything larger than o and
| denote it as inf.
|
| Edit: I found an explanation
| https://ionathan.ch/2021/08/04/sized-types.html
| mananaysiempre wrote:
| 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.
| nickdrozd wrote:
| > 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
| CHY872 wrote:
| 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.
| shadowgovt wrote:
| 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 wrote:
| 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.
___________________________________________________________________
(page generated 2023-06-06 23:00 UTC)