Page 6 of 6

Re: The position of constructive mathematics on the axiom of infinity is outright unsustainable

Posted: Thu Jun 26, 2025 3:19 am
by godelian
Skepdick wrote: Wed Jun 25, 2025 6:07 pm Your very premise is incoherent in my worldview.
It is informed by the excerpts that I have read in the body of literature. These excerpts have strong Platonic inclinations, are based on classical logic, have no qualms with the LEM, and by default assume the foundational layer of ZFC. The problem of going against the mainstream, is that you pretty much have to paddle on your own, or find yourself confined to some obscure minority view. I am just a reader of the stuff. I don't write any of it. So, adopting a small minority view means that there would not be much left to read.

Re: The position of constructive mathematics on the axiom of infinity is outright unsustainable

Posted: Thu Jun 26, 2025 8:50 am
by Skepdick
godelian wrote: Thu Jun 26, 2025 3:19 am It is informed by the excerpts that I have read in the body of literature. These excerpts have strong Platonic inclinations, are based on classical logic, have no qualms with the LEM, and by default assume the foundational layer of ZFC. The problem of going against the mainstream, is that you pretty much have to paddle on your own, or find yourself confined to some obscure minority view. I am just a reader of the stuff. I don't write any of it. So, adopting a small minority view means that there would not be much left to read.
That's kind of the point I am getting at.

Feynman once said "What I cannot create - I do not understand."

If all you are doing is reading (an outsider's view); and not (re)creating the constructions yourself (an insider's view). It's very unlikely you are actually understanding anything.

It's a bit like interacting with an API without seeing the implementation.

Re: The position of constructive mathematics on the axiom of infinity is outright unsustainable

Posted: Thu Jun 26, 2025 12:55 pm
by godelian
Skepdick wrote: Thu Jun 26, 2025 8:50 am It's a bit like interacting with an API without seeing the implementation.
Especially during the initial stage of development, you can use a remote API or a local library without even looking at the source code. The most important information at that point are one or more examples of how to use a particular function. The source code itself will not tell you that. With just the source code, you won't even get properly started with the task of using an API. The source code only matters when you get confronted with unexpected behavior, because only the source code can tell you why exactly things go wrong for your particular input data, especially, if the error message does not convey much information, or if there is not even an error message because the erratic behavior is actually considered fine; which obviously also happens.

For example, how to use the libC strlen() function:

Code: Select all

#include <stdio.h>
#include <string.h>

int main() {
  char my_string[] = "Hello";
  print("%z\n", strlen(my_string));
  return 0;
}
// Prints "5"
That is the kind of examples that get you started with the API. The source code of strlen() does not matter and will probably never matter because this simple function is unlikely to behave unexpectedly:

Code: Select all

https://codebrowser.dev/glibc/glibc/string/strlen.c.html

/* Copyright (C) 1991-2024 Free Software Foundation, Inc.
   This file is part of the GNU C Library.
   The GNU C Library is free software; you can redistribute it and/or
   modify it under the terms of the GNU Lesser General Public
   License as published by the Free Software Foundation; either
   version 2.1 of the License, or (at your option) any later version.
   The GNU C Library is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   Lesser General Public License for more details.
   You should have received a copy of the GNU Lesser General Public
   License along with the GNU C Library; if not, see
   <https://www.gnu.org/licenses/>.  */
#include <libc-pointer-arith.h>
#include <string-fzb.h>
#include <string-fzc.h>
#include <string-fzi.h>
#include <string-shift.h>
#include <string.h>
#ifdef STRLEN
# define __strlen STRLEN
#endif
/* Return the length of the null-terminated string STR.  Scan for
   the null terminator quickly by testing four bytes at a time.  */
size_t
__strlen (const char *str)
{
  /* Align pointer to sizeof op_t.  */
  const uintptr_t s_int = (uintptr_t) str;
  const op_t *word_ptr = (const op_t*) PTR_ALIGN_DOWN (str, sizeof (op_t));
  op_t word = *word_ptr;
  find_t mask = shift_find (find_zero_all (word), 
s_int);
  if (mask != 0)
    return index_first (
mask);
  do
    word = *++word_ptr;
  while (! has_zero (
word));
  return ((const char *) word_ptr) + index_first_zero (
word) - str;
}
#ifndef STRLEN
weak_alias (__strlen, strlen)
libc_hidden_builtin_def (strlen)
#endif
The implementation of the strlen() function yields a lot of mental overhead and noise that will probably not help you using the function. You are almost surely better off looking at a second example, if the first example was not clarifying enough.

Of course, the source code must still be available, as a matter of development policy. Sooner or later, with intensive use, you will indeed likely run into a situation that can only be solved by stepping through the source code. However, that is not how it typically starts.

Re: The position of constructive mathematics on the axiom of infinity is outright unsustainable

Posted: Thu Jun 26, 2025 2:01 pm
by Skepdick
godelian wrote: Thu Jun 26, 2025 12:55 pm The source code only matters when you get confronted with unexpected behavior, because only the source code can tell...
It really can't tell you any of that. Not unless you understand the semantics of the compiler.

At best the source code can help you infer the intended behavior, but not the actual one.

You speak like somebody who has never had to debug a compiler bug before.

Re: The position of constructive mathematics on the axiom of infinity is outright unsustainable

Posted: Thu Jun 26, 2025 2:36 pm
by godelian
Skepdick wrote: Thu Jun 26, 2025 2:01 pm You speak like somebody who has never had to debug a compiler bug before.
There are erratic behaviors in tools like GCC, but the ordinary user is unlikely to run into one of them.

Compiling and debugging GCC requires bootstrapping with another instance of GCC. The procedure is a bit intricate.

I have never volunteered to work on the GNU software or on Clang/LLVM. It would probably be fun but it would obviously also require quite a bit of time to become productive in that environment.

In typical real-world projects, I follow an Ousterhout strategy. I will use a scripting engine, unless I have a very good reason to relegate a task to native code, which often exists already, and has often been integrated already. New custom native data structures do however occasionally emerge out of the fray.