For the mathematician the meaning of the words representing the basic concepts is irrelevant; any interpretation of them which fits, i.e., under which the axioms become true, will be good, and all the propositions of the discipline will hold for such an interpretation because they are all logical consequences of the axioms. Thus n-dimensional Euclidean geometry permits another interpretation where points are distributions of electric current in a given circuit consisting of n branches which connect at certain branch points. [...] From this standpoint mathematics treats of relations in an hypothetical-deductive manner without binding itself to any particular material interpretation. It is not concerned with the truth of axioms, but only their consistency; indeed inconsistency would a priori preclude the possibility of our ever coming across a fitting interpretation. "Mathematics is the science which draws necessary conclusions," says B. Peirce in 1870, a definition which was in vogue for decades after.
Hermann Weyl, The Mathematical Way of Thinking (1940)
Hermann Weyl, The Mathematical Way of Thinking (1940)
Forwarded from Αλι (EN, EO)
Forwarded from Programming Deadlock
Type Safe Generic Data Structures in C
https://danielchasehooper.com/posts/typechecked-generic-c-data-structures/
https://danielchasehooper.com/posts/typechecked-generic-c-data-structures/
Danielchasehooper
I Write Type Safe Generic Data Structures in C
I write type safe generic data structures in C using a technique that I haven’t seen elsewhere1. It uses unions to associate type information with a generic data structure, but we’ll get to that. My approach works for any type of data structure: maps, arrays…
❤1
Forwarded from AlexTCH
Mario Carneiro is (slowly) proving the Lean 4 (kernel) correct in the Lean 4 itself:
https://www.youtube.com/watch?v=hAj81bYngDA
There are curious insights into Lean 4 metatheory and actual implementation.
https://www.youtube.com/watch?v=hAj81bYngDA
There are curious insights into Lean 4 metatheory and actual implementation.
YouTube
TYPES2025 - 5.17. Mario Carneiro - Lean4Lean: Mechanizing the Metatheory of Lean
TYPES 2025 - Day 5 - Session 4
Mario Carneiro - Lean4Lean: Mechanizing the Metatheory of Lean
Mario Carneiro - Lean4Lean: Mechanizing the Metatheory of Lean
🔥1
Forwarded from Programming Deadlock
visual-programming.pdf
127.3 KB
Visual Programming with Interaction Nets
https://repositorium.sdum.uminho.pt/bitstream/1822/14408/1/article_20.pdf
https://repositorium.sdum.uminho.pt/bitstream/1822/14408/1/article_20.pdf
👍1
Forwarded from GALLY
YouTube
MicroHs, a tiny Haskell Compiler – Lennart Augustsson (Language Pioneer & Compiler Expert)
In this engaging and technically rich talk, Lennart Augustsson presents his project microHs – an extremely lightweight Haskell compiler developed both as a fun experiment and a deep dive into functional programming.
Augustsson, known for having written several…
Augustsson, known for having written several…
Early_2025_AI_Experienced_OS_Devs_Study.pdf
5.3 MB
Becker, et.al, Measuring the Impact of Early-2025 AI on Experienced Open-Source Developer Productivity (2025)
Even though I'm not really a fan of academia, but I'm also not a blind believer of the Silicon Valley trope of dropping out because Gates and Musk did so.
Lawrence Paulson here urges people to take education seriously. Whether you are able to do that at Oxford, or by manually going through the classics yourself is up to you, in my opinion.
https://lawrencecpaulson.github.io/2025/07/02/Finish_your_degree.html
Lawrence Paulson here urges people to take education seriously. Whether you are able to do that at Oxford, or by manually going through the classics yourself is up to you, in my opinion.
https://lawrencecpaulson.github.io/2025/07/02/Finish_your_degree.html