ukj

26 ms·

211.
by ukj 5y ago
>until you choose to give it up PRECISELY You have to give up the safety to get the feature. So you "want type-safety". Until you don't. >static languages can have compile-time type safe dynamic dispatch "Compile-t
212.
by ukj 5y ago
You appear to be conflating compilers with runtimes. Dynamic dispatch happens at runtime. C++ and Rust are compile-time tools, not runtimes.
213.
by ukj 5y ago
Tractability vs possibility. You don't grok the difference. You can implement EVERYTHING in Brainfuck. Tractability is the reason you don't. The goalposts are exactly where I set them. With my first comment. "Every programmin
214.
by ukj 5y ago
Do you understand the difference between compile time and runtime? Neither C++ nor Rust give you static type safety AND dynamic dispatch because all of the safety checks for C++ and Rust happen at compile time. Not runtime.
215.
by ukj 5y ago
Everything comes at a cost of something in computation! That is what “trade offs” means. You can have any feature in any language once you undermine the default constraints of your language. You can implement Scala in Brainfuck. Turing com
216.
by ukj 5y ago
This is a trivial and obvious implication of Turing completeness. Why do you even bother making the point? With the right amount of indirection/abstraction you can implement everything in Assembly. But you don't. Because you like
217.
by ukj 5y ago
Every programming paradigm is a good idea if the respective trade-offs are acceptable to you. For example, one good reason why strong static types are a bad idea... they prevent you from implementing dynamic dispatch. Routers. You can'
218.
by ukj 5y ago
Yeah, but that is precisely how inductive types work. "Bonkers" premises. Iterate, iterate, iterate. "Bonkers" conclusions. GIGO. And yet the result is reified, exists and speaks for itself. So what is so "absurd&q
219.
by ukj 5y ago
Then you have some formally inexpressible/impredicative notion of "validation" in mind. For posterity (lifting from the depths of the threads): General case: Validating random data as input into some program. Particular case:
220.
by ukj 5y ago
You are over-complicating this into obscurity. General case: Validating random data as input into some program. Particular case: Validating random source code (data) as input into some compiler (program). Do compilers parse or validate? &qu
221.
by ukj 5y ago
The conference is indeed a spoof, but in so far as what Mathematicians call a "proof" - the paper contains one. Agda is a proof assistant in the spirit of the Calculus of Constructions ( https://en.wikipedia.org/wi
222.
by ukj 5y ago
+∞ parse verb. resolve (a sentence) into its component parts and describe their syntactic roles. In computer science what we do is precisely syntax analysis. Determining the meaning of operators. Mathematicians have the exact same problem w
223.
by ukj 5y ago
You are tripping up over polymorphism. "Is" means many things - which meaning you infer is precisely parsing! "A square is a rectangle" means "A square is a TYPE of rectangle" (at least, that is what I am parsi
224.
by ukj 5y ago
I am talking about the polymorphic use of the verb "is" during the process of formalization. "Red is a color" can be formalized as "Red is a type of color" or "Red is member of set Colors". You can&#x
225.
by ukj 5y ago
"A kind of" is precisely its formal use from the PoV of a type theorist. Two things are the same type of thing if they share all of their extensional properties. That is what it means for two things to be identical/equal.
226.
by ukj 5y ago
This paper is good for parsing/validating your source code (from the view-point of your compiler/interpreter). Code is data after all.
227.
by ukj 5y ago
The word "is" implies an isomorphism. If you see it differently you are implicitly assuming a non-formalist perspective on what "validation" means. Tell us about it.
228.
by ukj 5y ago
Software Engineers: Parse, don't validate. Mathematicians: Parsing is validation https://gallais.github.io/pdf/draft_sigbovik21.pdf
229.
by ukj 5y ago
It’s definitions/conventions all the way down. Which particular construction/definition of “the” reals/hyper reals are you referring to? The expansion of the “0.n…” notation is a separate matter. It also depends on which part
230.
by ukj 5y ago
>nobody can name a system where 1 and 0.999... are unambiguously defined, different numbers. The Hyperreals/Robinson reals. 0.999... < 1 - ε < 1 https://en.wikipedia.org/wiki/Hyperreal_number
231.
by ukj 5y ago
>Consequently, while I can reasonably safely apply a lower bar of trust to libraries and code, someone asking to be continuously trusted must be held to a distinctly higher standard. Also, this seems backwards to me. You trust Tailscale
232.
by ukj 5y ago
>I do tend to read the diffs first. You are lying to yourself. You are necessarily claiming that a single person (you) is capable of adequately verifying the trustworthiness of the work of hundreds (perhaps even thousands) of developers.
233.
by ukj 5y ago
They are exactly the same situation. When you run other people's code you are explicitly giving them control over your stuff. Ken Thompson pointed this out back in 1984. ( https://dl.acm.org/doi/pdf/10.1145&#x
234.
by ukj 5y ago
Ahhh, the illusion of control. The fine line between prudence and paranoia. Do you also manufacture your own silicon in fear of being owned by your hardware vendors? Write all your own software? In fear of being owned by zero days in open s
235.
by ukj 5y ago
Summary: It depends on what the function named “+” means/does. Software Engineers already have this intuition. We call it polymorphism. https://en.wikipedia.org/wiki/Polymorphism_(computer_science...
236.
by ukj 5y ago
It is 100% verifiable AND falsifiable. You can verify that Physics is captured in Mathematics. Mathematics is a Turing-recognisable language. If the universe is Physical then it is computable. This is a trivially true belief (see Church-Tur
237.
by ukj 5y ago
> if everyone is "religious", you've set a very low bar for what qualifies as religious And if everyone has “beliefs” then you have set a very low bar for what qualifies as belief which makes everyone a believer. You are
238.
by ukj 5y ago
> The question needs not be asked. That is a religious belief in denial of my factual needs. > A true areligious person does not ponder about the meaning of life, why we are here Great! So why does science matter to a true areligious
239.
by ukj 5y ago
> Either something means something, or it doesn't. This is a peculiar idea. What does my cat mean?
240.
by ukj 5y ago
> I don't understand the question. Truth is the correspondence of the mind with the real. That is only the correspondence theory of truth. There are many other truth-theories. There is the coherence theory, pragmatic theory, constru

More ›