scythmic_waves

I haven't read this yet but I see one of the two authors is George R. R. Martin? That's cool! Does he normally contribute to this kind of thing? I had no idea.

Oh _that's_ what's happening. I was wondering why so many images were broken but I hadn't investigated.

I appreciate write-ups of failed experiments like this. They're sorta like null results in science, but for engineering. And they can help others from needlessly walking down the same path.

If everyone only wrote about their successes, we'd all have to independently rediscover failures behind closed doors.

I bet reddit.com/r/ProgrammingLanguages/ would like this.

I hadn't seen this before, it's fantastic! Thanks!

I think because a full proof covering existence and uniqueness will either be really long or require tools from outside the scope of the text. E.g. there's a somewhat concise proof using linear algebra which I'll partially reproduce below. (I like this proof because the equation is derived from first principles rather than starting with an ansatz.)

---

Let x_n be a sequence defined by the recurrence relation:

    x_{n+1} = a * x_{n-1} + b * x_n

Observe that if we define a sequence of two-element vectors of successive elements:

    [x_0]  [x_1]  [x_2]
    [x_1], [x_2], [x_3], ...

then we can form the relation in terms of matrix/vector multiplication:

    [x_1] = [[0  1]] [x_0]
    [x_2]   [[a  b]] [x_1]

Let's name the sequence of vectors as y_n and call the matrix M:

    y_1 = M * y_0

We can get the next term in the sequence with another multiplication:

    y_2 = M * y_1
        = M * (M * y_0)
        = M^2 * y_0

By induction we have:

    y_n = M^n * y_0

M has characteristic polynomial:

    r^2 - br - a = 0

with roots:

    r_1 = (b - c)/2
    r_2 = (b + c)/2
    c   = √(b^2 + 4a)

Therefore we have by diagonalization:

    y_n = S * [[r_1^n  0    ]] * S^(-1) * y_0
              [[0      r_2^n]]

where S is the matrix of eigenvectors. From here, we can finish our existence and uniqueness proofs from the existence and uniqueness of the eigenvalues of M.

In fact, I came to the comments to ask. Thank you!

Can you say more? I’m interested.

… maybe

Could you generate MathML server side to avoid JS?

Why did they not link to any examples of what they're talking about?

Thank you! I was trying to find this the other day but couldn't.

> I suppose the reason is because it takes more time?

I assume so. I didn't even notice that the article didn't motivate that `async: false` is bad. I always avoid it if I can since you might as well perform independent tests concurrently.

From the docs [1]:

* `:async` - configures tests in this module to run concurrently with tests in other modules. Tests in the same module never run concurrently. It should be enabled only if tests do not change any global state. Defaults to `false`.

[1]: https://hexdocs.pm/ex_unit/main/ExUnit.Case.html#module-tags

This is a great write up. There appear to be a few camps forming in the comments and I’m in camp “SQL is confusing and attempts to explain it in terms of relational algebra have felt inadequate to me”.

It also gives me some good follow up material to read. I’m particularly interested in that one link that forms subqueries and lateral joins in terms of a new “dependent join” operator.

Interesting! I’ll have to look over it when I have more time.

From a quick glance, it looks like it covers much of the same material as this text [1]. I wonder how they compare.

[1]: https://www.cambridge.org/core/books/understanding-machine-l...

Docs: https://pkl-lang.org/main/current/introduction/comparison.ht...

(Never used Pkl myself...)

My personal exasperation is less about being unable to find alternatives (e.g. [1]). It's more that those alternatives aren't 1) as good, 2) free, or 3) part of the same platform.

And even if I use an alternative, my friends, family, and workplace do not. So I'm still fighting the use of Google products after I stop using them.

[1]: https://www.reddit.com/r/privacy/wiki/de-google

No kidding. I don't trust my own by hand calculations anymore. And why bother? I'd rather just write down the equation I need and let a computer do the rest.

Additional context: for a flavor of what I have in mind, you can glance at the wiki page for vector spaces [0]. E.g. [1].

[0]: https://en.wikipedia.org/wiki/Vector_space

[1]: https://en.wikipedia.org/wiki/Vector_space#/media/File:Deter...

Oh interesting! I like that it can embed LaTeX and code snippets.

However I fear it may not be low-level enough for what I'm hoping to do. Since I can't edit the OP, I'll reply to it with examples of what I'm hoping to achieve.

EDIT: https://news.ycombinator.com/item?id=38846756

To clarify: my goal is to create visual aids and embed them in an HTML document. So I want diagrams _for_ the web and not necessarily built _by_ a browser.

For instance, one person's approach could be to use the Inkscape software to create SVGs. Another approach could be to use JS to call the Canvas API. Another is to use Tikz.

Because there are so many approaches, each requiring a heavy investment in learning, I was curious if any in the HN crowd have strong preferences.

And that's a good place to stop :)

And not to distract from the point (which you made well), but weight lifting in general is tricky to compare since you generally want to take body weight into account. Benching 225 lbs is a different prospect for a 125 lbs individual vs. a 250 lbs individual.

I enjoyed that, thank you.

I like the video’s focus on resources. I’ve worked through several of those texts myself and can vouch for them. Though I was hoping a step by step guide might touch on things like making outlines, reviewing notes at a later date, etc.

Sidenote: I recommend linear algebra done wrong over Axler’s text. But that was just my personal preference. Both would be good introductions.

Wow I have no opinion on the product yet, but I’m really impressed with the design of the site. And I don’t say that lightly.

Your link says at the bottom that modals can be used for forms.

Came here to say this. I love the magic in that series.

There are post-quantum-computing encryption schemes [1], thankfully.

[1]: https://en.wikipedia.org/wiki/Post-quantum_cryptography

I've not had as much time to look into formal verification as I'd like and this blew me away

    lemma LemmaFromToBytes(v: nat)
    ensures FromBytes(ToBytes(v)) == v {
      // Dafny does all the work!
    }

The compiler can _prove_ one function is the inverse of another? That's so cool.

Also I disagree with some of the other posts dismissing the usefulness of this kind of thing. I grant that formally verifying every little piece of my code would be overkill. However, I absolutely want certain core pieces of my application formally verified.

I'm gonna have to play with Dafny at some point.