Hacker News: sordina

New comment by sordina in "Hylomorphism"

sordina — Mon, 18 Dec 2023 02:20:46 +0000

Also: 21 Hylomorphisms and nexuses from Pearls of Functional Algorithm Design: https://dai.fmph.uniba.sk/courses/FPRO/bird_pearls.pdf

New comment by sordina in "The deep link equating math proofs and computer programs"

sordina — Sat, 14 Oct 2023 07:54:59 +0000

Curry Howard shows that for a logical proposition (A) with corresponding constructive proof (B), there will be a type (A') with program (B'). It's not about proving desired properties of programs. However, you can use the CH principles to do this too, as long as you can encode the proposition about a program in its type. This will not often look like the dataflow type of the naive program though. Look at software foundations for real detail, I'm not expert at this stuff, just aware of the basics.

New comment by sordina in "The deep link equating math proofs and computer programs"

sordina — Sat, 14 Oct 2023 07:49:56 +0000

Mate, the point I was making is that 15 minutes is not a reasonable time frame to learn new programming concepts in.

New comment by sordina in "The deep link equating math proofs and computer programs"

sordina — Fri, 13 Oct 2023 04:09:55 +0000

You've got the right idea. A program is a proof for the proposition made by its type. Only for the right languages though, and not in the naive sense of `assert(1+1 == 2)` proves the assertion.

New comment by sordina in "The deep link equating math proofs and computer programs"

sordina — Fri, 13 Oct 2023 03:09:04 +0000

Well, I interpret that as the assertion that it's more opaque than other types of programming. But I disagree and think that it is actually simpler in terms of the syntax and amount of prior understanding required. My blunt reply is that to assert that a particular example is inaccessible but then only to have dedicated 15 minutes to prove so is silly. I'm sure most people who seem to suggest that this stuff is opaque had no problem learning PCRE or complicated SQL joins and also didn't complain that it took more than 15 minutes to do so. Of course TT is a deep field and there are many complicated parts of it, but the syntax, rules and the example given are not opaque and very understandable to anyone who can tackle languages and abstraction.

New comment by sordina in "The deep link equating math proofs and computer programs"

sordina — Thu, 12 Oct 2023 23:20:28 +0000

What part am I ignoring?

New comment by sordina in "The deep link equating math proofs and computer programs"

sordina — Thu, 12 Oct 2023 02:56:14 +0000

If someone can learn C type syntax this is MUCH simpler. That doesn't mean you don't have to spend a little bit of time learning how it works, but it is not some kind of number-theory level maths construction only accessible to savants.

New comment by sordina in "The deep link equating math proofs and computer programs"

sordina — Thu, 12 Oct 2023 02:54:03 +0000

15 minutes is not a long time. Easily understand doesn't mean instantly understand with no background reading.

New comment by sordina in "Before he was the Unabomber, Ted Kaczynski was a mind-control test subject"

sordina — Sun, 11 Jun 2023 13:34:51 +0000

Pithy but useless sentiment.

New comment by sordina in "There is no A.I."

sordina — Sat, 22 Apr 2023 01:26:28 +0000

So if you implemented it with analog circuits that would satisfy your criteria?

New comment by sordina in "There is no A.I."

sordina — Sat, 22 Apr 2023 00:32:59 +0000

So if you lost the weights how is that not killing the AI? Is it because it lacks the death experience? If so what about bitrotting the weights incrementally and degrading its inputs?

New comment by sordina in "Adventures in Advent of Code"

sordina — Sun, 04 Dec 2022 02:11:15 +0000

Yeah same! It really was a tricky one for me: https://github.com/sordina/advent2021/blob/solutions/src/Adv...

New comment by sordina in "Extism: Make all software programmable with WebAssembly"

sordina — Thu, 01 Dec 2022 23:56:26 +0000

The HTTP examples are fine, but a lower-level network module would enable all sorts of amazing plugins like a JDBC style ecosystem (WDBC?).

New comment by sordina in "Zoom and Enhance"

sordina — Wed, 16 Nov 2022 12:03:49 +0000

The binary representation is a neat idea. I found the trickiest part of this problem for me was interpreting an expanding boundary of the considered world: https://github.com/sordina/advent2021/blob/solutions/src/Adv...

New comment by sordina in "Ask HN: Inherited the worst code and tech team I have ever seen. How to fix it?"

sordina — Sun, 18 Sep 2022 02:23:57 +0000

> generates more than 20 million dollars a year of revenue

and

> team is 3 people

and

> post COVID, budget is really tight

Why? All technical details aside if this can't be addressed I wouldn't even bother trying unless I owned stock.

New comment by sordina in "Automatic Differentiation in 38 lines of Haskell"

sordina — Sat, 17 Sep 2022 23:50:07 +0000

One of my favourite Haskell "one-liners" is combining the AD package with Number.Symbolic:

    {-# LANGUAGE ImportQualifiedPost #-}
    
    module Module_1663406024_9206 where
    
    import Numeric.AD qualified as Ad
    import Data.Number.Symbolic qualified as Sym
    
    -- >>> f x = x^2 + 3 * x
    -- >>> Ad.diff f 1
    -- >>> Ad.diff f (Sym.var "a")
    -- 5
    -- 3+a+a

    -- >>> Ad.diff sin pi
    -- >>> Ad.diff sin (Sym.var "a")
    -- -1.0
    -- cos a

The package authors did not need to coordinate to make this possible which is pretty wild.

Saw it first here: https://twitter.com/GabriellaG439/status/647601518871359489 and https://www.reddit.com/r/haskell/comments/3r75hq/comment/cwm...

New comment by sordina in "Show HN: Quake 1 ported to the Apple Watch"

sordina — Mon, 12 Sep 2022 04:45:06 +0000

Yes, it would be interesting to see Apple's response. Now I remember what made me ask this line of questions in the first place.

In the release notes for J901 iOS I saw the following:

"it is legally impossible to release a J IDE for iOS as an open source project due to restrictions imposed on app developers by both Apple Inc and the Open Source community".

https://code.jsoftware.com/wiki/User:Ian_Clark/iOS/Review_No...

Although there was no justification for this comment, but maybe it's just true due to enforcement.

New comment by sordina in "Show HN: Quake 1 ported to the Apple Watch"

sordina — Fri, 09 Sep 2022 12:22:00 +0000

Thanks for responding! So if there was a quality OSS level pack that could be bundled then that would overcome the only obstacle?

New comment by sordina in "Show HN: Quake 1 ported to the Apple Watch"

sordina — Wed, 07 Sep 2022 07:38:33 +0000

Is there a technical reason why this couldn't be put on the app store? I've seen reference to Apple not allowing certain OSS code but never seen that confirmed so I'm curious!

New comment by sordina in "JSON Crack – Visualize JSON data into graphs"

sordina — Sun, 28 Aug 2022 22:56:55 +0000

Uses https://reaflow.dev