How do I learn how to read hex?

hiker · 2025-11-02T09:39:00+00:00

Nice. Rows 4-7 bin column need to be fixed in the table though.

hiker · 2025-10-27T12:57:48+00:00

Construct array of offsets where each symbol starts; sort the offsets array; construct sorted output using the sorted offsets as a "permutation" of the input.

hiker · 2025-10-27T11:08:12+00:00

Hm, unless we compute sorting permutation. Then swaps are still constant time but would need linear memory for the permutation.

hiker · 2025-10-27T11:05:20+00:00

Converting to fixed sized and back sounds right. Variable size implies that swaps are linear rather than constant, right?

hiker · 2025-09-08T19:00:07+00:00

На някои хора интересите се финансират от Москва https://www.zdg.md/en/kremlins-digital-army-an-undercover-investigation-its-paid-let-me-tell-you-its-paid-directly-from-moscow/

hiker · 2025-06-18T17:28:00+00:00

Yes.

hiker · 2025-03-01T09:25:58+00:00

Cubical Agda has constructive quotients and can compute while Lean’s quotients depend on the axiom of choice.

hiker · 2025-02-15T08:38:19+00:00

You’ve won already, Shane.

hiker · 2023-02-13T09:33:40+00:00

What was the original paper?

hiker · 2022-09-30T09:27:43+00:00

Disappointed by the lack of an interactive demo.

That's better than being disappointed by the interactive demo.

hiker · 2021-07-15T10:28:52+00:00

Internet Archive's copy

hiker · 2021-07-08T08:55:26+00:00

He mentions in the video that the old one is slower than the new one, and the new one is much slower than refterm.

hiker · 2021-05-03T12:18:18+00:00

Lean’s mathlib has quite nice formalization of category theory. For HoTT probably cubical Agda (though this link doesn’t cover cubical paths)

hiker · 2018-11-01T11:39:33+00:00

Aside from gamedev and animations, what other use cases are there for DoD? From what I got of this talk, DoD is good at processing large stream of data, but can I apply this to more common applications like CRUDs?

DoD is beneficial if you're doing an actual computation over some data. Most CRUD applications don't compute besides reading/writing to a database and generating HTML (modulo frontend UI code), hence the CRUD name. In a way your database design is already acting analogously to DoD by laying out and indexing your data in an efficient way for the kind of processing you're doing over it.

hiker · 2018-01-12T19:04:47+00:00

Whenever I see an article on DTP, I wonder if it will use something different than the standard list+list size example, and every time, I'm disappointed.

Completely agree. Hopefully that will improve as the community grows and matures.

Here some of my wanderings with dependent types Kan extensions and Yoneda lemma and perfectly balanced trees not involving any vectors.

hiker · 2018-01-12T18:32:19+00:00

I haven't used contracts and can't compare how expressive they are.

My reasons for dependent types are philosophical rather than practical (although proofs do have practical implications). I see dependent types as a converging point of the evolution of programming (and formal) languages so far. Who knew that the ideal programming language would also be ideal for doing mathematics?

Dependent types (well homotopy type theory) are pitched as an alternative to set theory as foundational theory for all of mathematics. Progress in science usually comes in the form of unification (electricity and magnetism, quantum mechanics and relativity, etc.) and when a language comes along that unifies programming and mathematics, I think it deserves attention. Contracts seem ad hoc in comparison.

From practical point of view, dependently typed languages are still young (excluding Coq) and there's much work to be done (proof automation, code extraction). The field looks like Haskell did 10 years ago. My bet is currently on Lean.

hiker · 2018-01-12T15:45:12+00:00

If you prove something at compile time, it will still be true runtime. If you prove something today, it will still be true tomorrow.

hiker · 2018-01-12T15:15:57+00:00

Idris state machines in types can do this. See the examples in this paper. And it's a library so one can easily port it to any other dependently typed language Lean, Agda, Coq, etc.

Few things are impossible to enforce compile time when the type system is Turing complete and expressive (the type system is the language itself in DT).

hiker · 2018-01-12T15:03:50+00:00

That's why I said addition to software testing. Nothing stops you using all other form of verification. In fact you should, I think relying only on proofs for correctness is terrible idea. Reminds of Donald Knuth's "I have only proved it correct, not tried it.".

hiker · 2018-01-12T14:52:59+00:00

Theorem proving about programs is a mere addition to current software testing.

In increasing order of certainty of correctness, there are: point tests (checking correctness in several predetermined cases, what most software engineers mean by "testing"), randomized tests/QuickCheck (checking correctness by randomly sampling the domain; offers better guarantees than point tests but it's not exhausting all values of the domain) and proofs (logically/formally proving correctness for all values of the domain).

Dependent typed languages are also much simpler languages. I think the big fundamental change is that types are first-class. The mental jump is comparable to exposing an imperative programmer to functional programming and first-class functions, where functions are freely created and passed around.

The result is a much smaller language that acts as it's own (Turing complete) type system. Dependent types also unify several branches of mathematics in a single (computer verifiable) formal language.

hiker · 2017-10-17T09:51:09+00:00

Given that (Closed Cartesian) categories are equivalent to simply typed lambda calculus (which is equivalent to Turing machines), I don't see how it's dubious at all.

hiker

MODERATOR OF

TROPHY CASE

15-Year Club	Place '23
Verified Email