1. 2

    First idea that popped into my head is that this is only applicable if the thing in question is constructible. Non-existence is not constructible by its nature: I can prove to you that no decision procedure for the halting problem exists, but I cannot show this constructively.

    1. 1

      I would really like to learn more about this, aren’t coq proofs constructive by nature?

      Here is a proof that the halting problem for turing machines is undecidable: https://github.com/uds-psl/coq-library-undecidability/blob/30d773c57f79e1c5868fd369cd87c9e194902dee/theories/TM/TM_undec.v#L8-L12

      There are other proofs in that repo that show other problems as being undecidable.

      1. 2

        Huh, TIL. Indeed, it seems that there exist proofs of the undecidability of the halting problem that are constructive.

        ¬ (A ∧ ¬ A) is apparently provable in intuitionistic logic, which suffices for diagonalization arguments:

        lemma "¬ (A ∧ ¬ A)"
        proof (rule notI)
          assume 1: "A ∧ ¬ A"
          from 1 have "A" by (rule conjE)
          from 1 have "¬ A" by (rule conjE)
          from `¬ A` `A` show False by (rule notE)
        qed
        

        The general point still stands though, as there are other examples, such as non-constructive existence proofs.


        In general Coq proofs are not necessarily constructive, since one can define the law of the excluded middle as an axiom in Coq (and this is done in e.g. Coq.Classical). I can’t say anything about the proofs you linked though, as my Coq-foo is very limited.

        1. 1

          I think, the way the definitions expand in that repo, that undecidable (HaltTM 1) is decidable (HaltTM 1) -> decidable (HaltTM 1), which is trivially true. That is, it’s taken as an axiom that Turing machines are undecidable. (I think? I might be misreading)

        2. 2

          while Coq proofs are constructive, proving “~ exists t, t determines halting” does not construct any Turing machines, what it constructs is something that takes a hypothetical existence proof and builds a proof of false from it.

          i.e. in construct math, ~ P is a function P -> False. this function can never be invoked as you can never build a P object.

        3. 1

          As this post was tagged practices (not math) and the article addresses the difficulty of convincing people, I suspect you’ve misunderstood the author’s use of the phrase “constructive proof.”

          Mathematical (constructive proof) vs rhetorical (constructive criticism).

          1. 1

            I don’t feel like the author talks about constructive criticism at all, how did you come to that conclusion?

            1. 1

              As this post was tagged practices (not math) and the article addresses the difficulty of convincing people

              ☝🏾

              1. 2

                Just for future reference, “constructive proof” is a term from math and I meant my usage of the term to be an analogy to math. Math also involves convincing people. But maybe I should have tagged it computer science or math, sorry.

        1. 2

          It is better to use bigquery’s mirror of Hacker News, than to query the endpoint millions of times. Here is an example of using that data in bigquery: https://hoffa.medium.com/hacker-news-on-bigquery-now-with-daily-updates-so-what-are-the-top-domains-963d3c68b2e2 But you can also get the whole dump from there, and then import it into whatever data warehouse you want.

          1. 2

            Nice, but I wanted to specifically go with Snowflake as my database rather than BigQuery. Good point that I could have used BigQuery to get the initial dump and then load it into Snowflake.

              1. 1

                Neither the linked log or release notes page seems to have anything to say about this particular version. They both seem to stop notes at 9.4?

                1. 2

                  The release notes have one item listed for 9.5.4:

                  3.6. String ports from immutable strings (9.5.4)

                  A bug that miscalculated the buffer size for open-string-input-port given an immutable string has been fixed.

                  As for the log, the most recent version’s log is all the way at the bottom of the log at https://github.com/cisco/ChezScheme/blob/v9.5.4/LOG#L2112

                  Overall, this seems like a very minor release.

                  1. 4

                    This is the first release since Racket use Chez as backend compiler. The __collect_safe flag helps with C FFI performance, so does immutable strings et al. for most code. Also there is non-official (apparently) support for 32bit raspberry pi.

                    Otherwise, it is stable for some definition of stable.

                    1. 1

                      there is non-official (apparently) support for 32bit raspberry pi

                      ARMv6 is listed in those release notes.

                    2. 2

                      I dug into this and wondered why I couldn’t find 9.5.3 in the tags: https://github.com/cisco/ChezScheme/issues/531

                      It turns out this release also includes all the 9.5.3 changes as well! So given that, this is a very substantial change.

                  1. 3

                    I remember first learning about assembly in high school from my ti 83+ calculator. Sad to see it gone for the next generation of students.

                    1. 1

                      Considering the generalize variant of Collatz Conjecture was proved undecidable, I bet my money this guy won’t get anywhere.

                      1. 1

                        From the end of the article:

                        He and his collaborators are working on a paper summarizing what they’ve discovered so far, but they’re nearly out of ideas and will likely have to give up on Collatz soon — for now, at least.

                      1. 3

                        Any particular reason to share this here? I don’t see anything particularly news-worthy in the release notes of this point-release.

                        1. 9

                          Although it’s a x.y.1 release, it includes a lot of new features.

                          I’ve been using the new Bits* data types to write a more accurate mysql wrapper around libmysqlclient at https://github.com/thomasdziedzic/mysql-idris2/

                          Also the new :browse and :doc interpreter commands are super useful for exploration.

                          1. 1

                            Any idea why it’s not 0.3.0 then?

                            1. 2

                              I guess they’ve made a quick release for the Scottish Summer School on Programming Languages and Verification http://www.macs.hw.ac.uk/splv/ to get the new proof/program search heuristics in.

                          2. 3

                            Since Idris 2 is in its infancy, the language and tools are taking massive leaps forward right now. This release adds some critical features (as mentioned by sibling comment) to the REPL and gets the IDE Mode support almost to par, if not at par with Idris 1. Really exciting, as I’m working on two projects in Idris 2 right now and have been craving better editor integration. Idris is a language that truly comes alive with the editor integration.

                            1. 2

                              I think the more exciting part of this release is the code generation/search, specifically the :psnext and :gdnext REPL commands and their IDE mode counterparts.

                            1. 4

                              Working through “Practical TLA+”.

                              1. 6

                                Hoping to go kayaking, weather permitting.

                                Continuing to work my way through “Practical TLA+”.

                                1. 3

                                  I’m getting a copy of Practical TLA+ so I’ll be reading that this weekend.