enricozb

Kakoune _barely_ has a scripting language. It has essentially a set of commands and some basic string substitution, one of which will let you drop to a shell (something akin to substitute this string with the result of evaluating its contents through bash). With this you can write your scripts in whatever language you like. My plugins are almost all in Rust, some are in bash.

One thing I was looking for just yesterday was a way to dump my terminal's (alacrity) scrollback - escape sequences and all - to stdout. I wanted to pipe it to my text editor to search. Alacrity doesn't seem to have this unfortunately, but wezterm does with get-text.

Love this sort of "eye candy". Reminds me of the kind of style I was looking for when theming my jailbroken iOS devices. I loved William Silvester's "Jaku", it had similar skeuomorphisms in its design, and the texture of the materials in the icons were pixel-perfect.

What I was referring to is that we don't know if ZFC, for example, is consistent. And it is only consistent if there are unprovable statements. And of course, you can't know which statements are unprovable (because then you would prove its consistency). So, in some sense you're always chasing your own tail. Theorems might be proven true only because ZFC is inconsistent and therefore everything can be proven.

The Lean language is known to be equivalent to ZFC + {existence of n < omega inaccessible cardinals}, which is roughly the common language of mathematics. The actual implementation of the kernel _may_ have bugs, but that's sort of separate from the language definition.

The sentiment I see for the purpose of Lean now and in the near future is for more collaborative mathematics. Theorems and structures are more transparent and concrete (the code is right there). Results are more consumable. The community does not seem to see its main purpose being a way to quell doubts of a paper proof.

Such is the nature of math as well.

While there indeed may be bugs, it's my understanding that any trust needs to be placed only on the kernel.

> various stacks of libraries that other humans have written

If you're referring to mathlib here, I'm not sure this is correct. As again all mathlib code compiles down to code that is processed by the kernel.

Indeed this is reinforced by the draft paper on the website [0]:

> Lean is a large project, but one need only trust its kernel to ensure that accepted proofs are correct. If a tactic were to output an incorrect proof term, then the kernel would have the opportunity to find this mistake before the proof were to be accepted.

[0]: https://zeramorphic.github.io/con-nf-paper/main.l.pdf

I don't have a PhD in biology (or in anything), but isn't temperature a single number "explaining" a gazillion interactions we will never "understand"?

I really wish there was a more react/swiftui-esque TUI library. One day I'll get around to fixing the fundamental flaws in my crate [0]

[0]: https://docs.rs/intuitive/latest/intuitive/

Surfing. Never been so addicted to a form of exercise before.

There's a cool repository of wildlife sounds here (including birds): https://xeno-canto.org/

;)

Everything about this group is fascinating. They are digital nomads on a boat. Every article [0] is a peek into an existence I didn't think or even consider was possible. I always get thrown into a rabbit hole when I visit their site.

In another life maybe.

[0]: https://100r.co/site/dry_toilet_installation.html

Reminds me of his "Change" off of "26 mixes for cash": https://www.youtube.com/watch?v=ecHLSoJeAAA

However, that's from a sampled drum beat. I generally agree though that this generated snippet doesn't remind me of Aphex Twin much at all.

I tried (and sort of failed) to build something like this for rust [0] (warning it's broken at the moment).

It's a lot harder than I expected. Especially since the terminal has no notion of focus, and with Rust it's really hard to not just clone everything you get your hands on when writing a UI library. The borrow checker really feels like it gets in the way of features like signals [1], and partial re-renders.

[0]: https://docs.rs/intuitive/latest/intuitive/ [1]: https://preactjs.com/guide/v10/signals/

I think there is a typo when defining v(e), it says both v(e) = e and v(e) = empty set.

Some related links (specifically that they perform "high school" algebra on types):

- Seven trees in one [0], a paper showing a bijection between binary trees and seven-tuples of binary trees.

- The algebra of algebraic data types [1] discusses Taylor expansions of data types.

- Differentiation of higher-order types [2] is commenting on OP's paper.

I used to be really interested in type theory, but haven't had as much time to explore it, but over the years I've saved these links (and the one posted).

[0]: https://arxiv.org/pdf/math/9405205.pdf

[1]: https://codewords.recurse.com/issues/three/algebra-and-calcu...

[2]: http://conal.net/blog/posts/differentiation-of-higher-order-...

It's not quite ready yet, but I'm writing something similar for Rust [0]. It's much more similar to React (with respect to components, and hooks), and the DSL is inspired by SwiftUI.

Disclaimer: Version 0.6.x has a pretty severe flaw where the constraints around hook order are way too strict, and this also prevents conditional renders [1]. I'm working on a full rewrite which will be released as version 0.7.0, which exists on github as a branch right now [2]. Docs also exist for an alpha version of 0.7.0 [3].

[0]: https://docs.rs/intuitive/latest/intuitive/

[1]: https://github.com/enricozb/intuitive/issues/4

[2]: https://github.com/enricozb/intuitive/tree/0.7.0

[3]: https://docs.rs/intuitive/0.7.0-alpha.0/intuitive/index.html

Wouldn't it be more accurate to state that it's NP-complete? In the first step of the proof they show that SR-Dec is in NP.

What's this ascii char 0x11 (device control 1) char at the end of this post's title? It's also present in the article's title.

Absolutely! I saw that lazygit recently(?) added scrollbars, and I'm actually working on adding this as a new component.

Similarly to how React does it I'd imagine. There is a static vector of `State` elements that is initially empty and is filled on the first render with each call to use_state. When calling use_state on subsequent renders, this vector is read from. This is also why, like React, use_state calls must always be in the same order across renders.

I've written a few TUIs in Rust, and the amount of code needed for the UI components always felt excessive. For a while, I had been toying with the idea of being able to write components in a SwiftUI-like DSL and have state managed like React does with hooks. Intuitive is the result of that frustration and desire.

Right now it's in between a proof-of-concept and an alpha version of the crate. I'm in the process of re-writing one of my TUI apps using Intuitive, and so far it has proven itself as a way to greatly reduce the amount of code necessary for a TUI.

I would be grateful for any feedback on the idea, the design, and/or the implementation. I hope it's well-received!

Is there any situation in which signals couldn’t replace useState?

Same here, I'm so bored that I typed in "I am bored" into https://hn.algolia.com/ and found this post.

Love his stuff, especially Sidney’s Sizzler and the United Acid Emirates album. His brother, Squarepusher, is a bit different but also really good.

There's pass, a CLI password manager that's version controlled and encrypted with your PGP key: https://www.passwordstore.org/

There are also (unofficial) iOS and Android clients that sync to a git repo.

Curious which bitmap font you use? I use terminus.

I think it might actually be better to reward someone for updating extremely old documentation. Like if there have been N commits since this documentation was updated, it should be worth N points. Then people are incentivized to update the oldest documentation. Sure someone could wait for yet another commit and have it be worth N+1 points, but someone else might take it up.

Any time I am reading a new book, I use Calibre to change the font to EB Garamond [0] before moving it to my e-reader.

[0]: https://fonts.google.com/specimen/EB+Garamond

I currently see

> We are currently offline for maintenance

On https://stackoverflow.com/, but I see nothing on https://stackstatus.net/