ukj

59 ms·

541.
by ukj 7y ago
The balance between beauty/structure and effectiveness is tough to get right. There are cases where functional programming is essential, and there are cases where it's an absolute overkill. Developing the judgment to tell which is
542.
by ukj 7y ago
https://en.wikipedia.org/wiki/Hot_spot_(computer_programming...
543.
by ukj 7y ago
It's the SoC principle[1] applied to organisational design. It faces the same challenges as it does in software - strong/weak coupling. Leaky abstractions. Duplicate functionality. Hotspots. It gets complex for all the same reason
544.
by ukj 7y ago
Have a look at this page [1]. Mathematica is exceptionally powerful and has a very rich vocabulary. In so far as expressing ideas across the computational paradigms - you will struggle to find a match. It's just a pity that its grammar
545.
by ukj 7y ago
"Iatrogenics" is a handy metaphor to capture the sentiment above. https://en.wikipedia.org/wiki/Iatrogenesis
546.
by ukj 7y ago
I calibrate my language in real time to that of my interlocutors. Some times drawing the distinction is necessary, some times it's not. Conceptually (for one's own intellectual benefit), recognising the distinction between know-wh
547.
by ukj 7y ago
I am well aware and require no introduction. That it has been debated for thousands of years is a fact. That it is yet unsettled as of 2019 is also a fact. Even worse than the Gettier problem, the proposition "Tomorrow I may or may not
548.
by ukj 7y ago
Without resorting to actually playing the silly philosophical word-games, here is how one debate might play out: Me: Why is "there is an iceberg in the water" knowledge? You: "because it corresponds to reality". Me: Tha
549.
by ukj 7y ago
Which begs a whole lot of other questions: * What is understanding? * How do I know that I understand? Sooner or later you realise that all theories of knowledge have one fundamental flaw - the problem of criterion[1]. And if you so choose
550.
by ukj 7y ago
Nobody pays attention to Goodman's problem of induction [1]. The truth is that nobody really knows how we ought to arrange society, and which arrangement is likely to work. Everybody is guessing! The moment you arrange the system one w
551.
by ukj 7y ago
At a glance, it seems like it could be a drop-in replacement for Spectacle, but with extra features. Lets give it a try...
552.
by ukj 7y ago
Is it a case where perfect is the enemy of good enough? I've never felt the need to move anything programatically e.g automatically without it being triggered by my intention. Spectacle has "next/previous display" shortc
553.
by ukj 7y ago
That gets your hand away from home row. I have gone the other way. One of the thumb-buttons on my Ergodox EZ is"Super + C" makro. The other is "Super + V". One-thumb copy/paste.
554.
by ukj 7y ago
If tiling is what you are after, was Spectacle not a good enough solution on OSX? I use a QMK-based keyboard (although I am sure you can achieve similar levels of functionality with Karabiner) where choosing my window placement is a 2-key m
555.
by ukj 7y ago
Intuition also tells you the correct result for many a complex computations. Because intuition is "simulation" after all. Gedankenexperiment. You know the correct result for dropping a glass on the floor. Insight comes from knowin
556.
by ukj 7y ago
Because physics is about formalising intuition. If you don't write the algorithm predicting the empirical consequences - you haven't solved the problem. The mystery is in the absence of an algorithmic solution. Think: Reverse Math
557.
by ukj 7y ago
I think you are missing the point. Solving a problem using mathematics is EQUIVALENT to solving a problem using computation (which is a silly truism, because your mind is a computer). They are two different mind-instruments, two frameworks
558.
by ukj 7y ago
The exact same thing can be said about any human dynamic where the objective is to teach. The end-goal is to make the material accessible to the learner by connecting it some pre-existing human intuition or experience, thus providing the le
559.
by ukj 7y ago
By the way - this is rather circular and it begs questions. > We call the sort of thinking mathematicians do "mathematics" What kind of thinking do mathematicians do? Is it any different to the kind of thinking computer scienti
560.
by ukj 7y ago
More succinctly: The thing you want proven is a proposition. A proposition is a type. Writing the algorithm which implements the type is the same as proving it. https://ncatlab.org/nlab/show/propositions+as+types
561.
by ukj 7y ago
Where Hilbert erred was looking for foundations in first-order logic. Univalent foundations are laid on high-order logic. It's the distinction between top-down and bottom-up thinking. If you are into philosophy/epistemology - it&#
562.
by ukj 7y ago
>when push comes to shove, anything goes as long as it's clear to another mathematician. Well, yes! That's not inherent to Mathematicians. That's how all human communication works. That's what we use "natural&quo
563.
by ukj 7y ago
It always boils down to use-cases. Ultimately, what formal verification gives you is a guarantee of structural correctness, but not behavioural correctness. Whether a program behaves as intended or required is still a task for humans. Garba
564.
by ukj 7y ago
A theorem is a consequence of a set of axioms. By definition. It may be an a-priori truth in the context of the particular proof you are working on, but a-priori your theorem there is always an axiom. Wanting to prove that X is a theorem of
565.
by ukj 7y ago
The Chomsky hierarchy covers all of that. It's linguistics for formal languages. Grammar, syntax and semantics together with reflection allows for formalisms and meta-formalisms. It all culminates in Turing Completeness. Chomsky Type 0
566.
by ukj 7y ago
A-priori truths are called axioms. In the context of the Curry-Howard isomorphism you don't "prove things about programs". Programs ARE proofs. Not all programs, mind you. You need to be using a dependently-typed language lik
567.
by ukj 7y ago
A lookup table is a particular case of a space-time trade-off. https://en.wikipedia.org/wiki/Space%E2%80%93time_tradeoff
568.
by ukj 7y ago
Once you are done thinking your thought() function returns a result in the form of language, no? Or does thought() fail to halt?
569.
by ukj 7y ago
What mathematicians DO is computation. What a mathematicians WRITE is a formal language used to express computation. Manipulating mathematical expressions has a name. Symbolic Computation. https://en.wikipedia.org/wiki/
570.
by ukj 7y ago
The thing is - if Programming corresponds to Maths (according to Curry-Howard) what is really happening is Mathematicians and Programmers are disagreeing over language, not over substance. Mathematics is a formal language. As such - it&#x27

More ›