Cheng Zhang

I enjoy algebra, coalgebra, and fixpoints (and I wish I am better at it). Assistant professor at Worcester Polytechnic Institute (WPI) studying programming language semantics and applications in verification, testing, and optimization.

sloppier than slop, vibier than vibe.

"We have killed epsilon with a dagger, the delta is next."

"I cannot Grothendick construction under these conditions."

Pronouns: he/him or they/them

Public Key

npub1ucfl35l5pyknn8j3yhghqjljmllxsmmtjggkuxfpu782nnrfj0wqd8q6qy

NIP-05 Address

czhang03_at_mathstodon.xyz@momostr.pink

Profile Code

nprofile1qqswvylc606qjtfenegjt5tsf0edllngda4eyytwrys70r4fe35e8hqpz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0ds96nlfd

Publishing to

relay.damus.io

nos.lol

Author Public Key

npub1ucfl35l5pyknn8j3yhghqjljmllxsmmtjggkuxfpu782nnrfj0wqd8q6qy

Show more details

Last Notes

2026-06-05 15:58:48 UTC

- reply

Miktex installs packages on the fly!

2026-05-24 12:35:24 UTC

- reply

I thought OCR + semantic search would be helpful (although my tablet likely will not support semantic search), but looking back that my note is too doodlely it is unlikely to play well with semantic search (or OCR).

2026-05-24 12:27:38 UTC

- reply

I do have this, even digitalized. But I still find it quite hard to navigate. To take two concrete examples:
- one of my collaborator recently asked me what is the problem with a certain approach, I need a couple hours to recall the problem. And this is after I go back to that a approach a couple times, each time blocked by the same problem, because I forget about it.
- I had a very intricate counter example in my note. I remember the intuition to construct it, and its rough shape, yet I cannot find it in my note. Then I spent a couple hour to reconstruct that.

2026-05-23 10:51:55 UTC

I wonder if people have some experience keeping research journals.
Kind of a "human trace" where I record the dead end and counter examples, so that I don't repeat my mistakes (I have been doing that a lot), and hopefully share that with the world.

2026-05-22 15:53:48 UTC

- reply

@npub19mh…v9e6
The vast majority of ACM research article and management are funded by the public, thus I feel it is reasonable to expect ACM serving public good and public access, instead of enriching a few oligarchs.
I understand this powerful minority have built the momentum to link aspects of public good to their personal benefit, like now, "making research accessible" is inevitably linked "provide research to them".
Although these enterprises might appear comparatively "open" and "useful" now, history have shown, they would happily cripple competition and abuse consumers when it is profitable for them.
And ACM, IMHO, must not aid in such effort.
I urge ACM to think about how to not provide an unfair advantage to the few in accessing these valuable and powerful knowledge, even when they are armed with unfathomable amount of resources and when the social scale is already tipping towards their favor.

2026-05-21 11:03:39 UTC

- reply

I have to admit I am very surprised that AI can keep a coherent view of complex mathematical concepts even when mathematical literature is sparse.
Deep down, I have a (hopefully irrational) fear that human will eventually be at a disadvantage: we only have a brain so large, and it need constant refresh.
It would be hopeless to have the same breadth of knowledge as the internet.
Eventually, will these companies kick "human out of the loop", which would make mathematics only as recreational activities -- a "solved game" for the industrialists.
I am fortunate enough to have a job, but what should I tell my students?
How do I motivate the value of the knowledge I built up, and how many of it will be valued in the future of computing?
What worries me even more than the potential end of professional mathematics, is the fact that LLM might not be democratized in several life times.
While previous attempts to monopolize knowledge seems vulnerable by today's view, the best model seems to succeed, at least for now, are only controlled by a few for-profit company.

2026-05-17 13:19:36 UTC

- reply

Do you have a reference for call-by-push-value that you enjoy?

2026-05-16 12:24:50 UTC

- reply

Apologies for being slow.
My understanding is that infinity or `inf` is a value of type Nat, and the order of value are usually flat, i.e. `Zero` is not smaller than `inf = Succ (Succ (Succ ...)))`.
I believe this is confirmed by the ordering we defined: there is no ⊥ in `Zero` to replace.
In other word, I believe infinity is the unique solution of `inf = Succ inf` in the DCPO we defined.
I guess another example would be potentially infinite list over Booleans: in this case, we have infinitely many infinite list instead of one infinity in extended natural numbers.
I don't see which particular infinite list can be the top element.

2026-05-16 11:15:23 UTC

- reply

> the order n ⊑ m if n = m, or m = ∞, or m can be obtained by replacing a ⊥ in n with another element.
I struggle to understand the second condition m = ∞ though, ∞ is a value within haskell, thus I don't know why it would matter in this dcppo order.
I thought the order is only the n ⊑ m if m can be obtained by replacing _some_ ⊥ in n with another element.
By changing "one" to "some" this includes the case n = m and supports data type with more than one recursion, like binary trees.

2026-05-16 11:00:04 UTC

- reply

That is extremely helpful and made me understand much better the distinction between free and strict languages. The different placement of the free functor F is particularly enlightening.
PS: yeah laziness by default is likely a mistake, unfortunately.
It was cool when I first started using Haskell, now I feel it just enables the construction of untraceable patterns with often subpar performance :(

2026-05-16 10:37:34 UTC

- reply

That is interesting. I guess the mistake I made here is that Haskell (intuitively) does not admit the equation `⊥ = Succ ⊥ `, thus ⊥ is not a solution at all.
I imagine, this is not true in strict languages? In some sense, strict language from a dcppo with one more equation `⊥ = Succ ⊥ ` than lazy language, thus their least solution are often different?

2026-05-16 08:38:35 UTC

- reply

very helpfully pointed out algebraically compact category like those enriched by pointed CPO, when a last posted a question similar to this.
But I am not entirely sure how algebraically compact category would fit into all of these :(

2026-05-16 08:30:11 UTC

- reply

I wonder if this points out a weakness the standard categorical semantics of type theory (which I am not super familiar with).
To be specific, as far as I understand, standard syntactic model would be well typed terms modulo the desired equivalences like αβη, but this seems to assume confluence via these equalities.
Yet, I am not entirely sure confluence still hold given the existence of fixpoints.
Again, I know very little about this, so please scold me if I said anything horrendously stupid.

2026-05-16 08:28:26 UTC

I was talking to my students about inductive and coinductive data types, and she asked what about `inf = Succ inf` in Haskell, now I cannot sleep.
The naive answer is that "this is actually a corecursion, thus defines infinity". However, the uncomfortable truth is that **Haskell semantics don't know whether definition is recursive or corecursive**.
Sometimes Haskell solves the fixpoint equation `inf = Succ inf` to infinity, instead of the least solution, which should be infinite loops.
Yet in other cases, Haskell will solve the fixpoint equation into its least solution: consider the following definition, which generates a infinite fixpoint equation where the variables are `eq n m` for all `n m in Nat`
```hs
eq Zero Zero = True
eq (Succ n) (Succ m) = eq n m
eq _ _ = False
```
the variable `eq inf inf`, in this case, is solved to its least solution infinite loop, instead of `True` like a proper corecursive language.
Intuitively, Haskell tries to explore the coalgebra generated by the fixpoint equations to compute its solutions.
**It seems like that Haskell solves to the final coalgebra when the reachable state is finite (i.e. regular), but solves to infinite loop when the reachable state is infinite.**
As a corollary, neither the standard DCPO semantics nor the standard final coalgebra semantics seems to fully capture the semantics of Haskell.

2026-05-15 11:06:27 UTC

I love that most of the example (and all the useful example) we have of _completely iterative algebra_ are domains where solution are _not reachable via iteration_.

2026-05-11 01:52:08 UTC

- reply

I thought canvas is released under AGPL? https://github.com/instructure/canvas-lms

2026-05-09 09:32:38 UTC

Best papers would have one reviewer rejecting it claiming it is obviously true, while having another reviewer rejecting it claiming it is obviously false.
Corollary: the best paper would have a hard time getting published.

2026-05-06 12:46:19 UTC

To make sense of the famous "snake eating its own tail" picture, we only need to look at its unique snake homomorphism into the final snake, which are rational snakes, that is, they have finitely many sub-snakes up-to snake isomorphism.
This is in glaring contrast to irrational snakes, which bits you for no f**king reason.

2026-05-02 18:16:26 UTC

- reply

I regret phrasing the original post in such a combative manner, that was not helpful. But I feel my conclusion still stands.

2026-05-02 17:05:47 UTC

https://arxiv.org/abs/2604.24658
I am angry article like this exists, and I am even more disappointed (mostly in myself) that I used to regard some of these authors as competent.
I have always regard mathematics, and by extend my research, as a human process: while knowledge discovery is a important aspect of research, **the joy, elegance, of aesthetics of the result is arguably more important**.
I am willing to dedicate my life to this endeavor not because it will take human to mard or it will make Jeff Bezos even richer.
**I am in this business because I used to be the student in the sparkle in my eyes when I see elegance and insights; now I get to see the same sparkle in my students.**
This paper pushes a reductive, monetary, corporate, and dangerous narrative about research, while ignoring important motivations that keeps academia flourish for millennia: the joy of human discovery.
**The willingness to let machine replace that process is communicating to me that these researchers do not see their result as their unique self-expression, and ultimately do not value their research.**
I certainly do not claim my researches are "good", but I always seek elegance, simplicity, and unique perspective in my research, even if I never get there because of my personal abilities.
I fail to see how this quality and self-expression can be upholded in these authors' framework, thus I would not waste my time by collaborating with any author of this paper.

2026-04-22 23:08:46 UTC

- reply

I suspect I know who you are talking about, and I am happy to report, they are still saying that now :) (but only in the context of trashing other proof system)

2026-04-20 00:12:53 UTC

- reply

Science is happening!

2026-04-16 15:04:28 UTC

The typical "smart person" depiction in popular media behaves exactly like a computer: they can calculate really fast, and/or remember a lot of things quickly and accurately.
I suspect this depiction might stem from the lack of understanding for human ingenuity by the public, which can also explain why many conceive LLM, a device aimed to remember and imitate human text, is "intelligent".

2026-04-16 11:32:32 UTC

- reply

slopal method v.s. formal method.

2026-04-11 13:15:28 UTC

- reply

I think Mythos is probably good, and much better than what I expected LLM can do in recent years.
But to me this is an cool alternative, and compensate the current security research.
Where security research can archive much better result per dollar, security research never gets the same amount of attention and investment as these LLMs.

2026-04-11 12:59:41 UTC

- reply

Okay I am most talk about inference cost, and trying to be conservative in estimate. Yes, but training cost should be around 10k if not 100k more expensive than traditional research.

2026-04-11 12:54:00 UTC

I am trying to be very cautious in being under representing current AI's ability, but I find the whole marketing behind mythos a bit over blown.
It is not uncommon for a year-long research project in verification and fuzzing to find tens of bug in critical software. Then we learn from them, integrate it into standard fuzzer and checker, so bugs of these nature reduces dramatically.
I guess I am not understanding (or arguably, a bit salty) that suddenly there is something that consume 100 times more resource than what we have developed found more bugs, they are "too dangerous", as if security research and software in general are doomed.

2026-04-02 22:46:08 UTC

New Career Goal: developing a framework surrounding Elgot iteration (often written as dagger) called Caesar.

2026-04-01 19:41:32 UTC

- reply

And violation of AGPL for not including your logo.

2026-04-01 11:47:09 UTC

Happy to report, my latest research is done completely autonomously with ✨AI✨: I snapped a picture of a commutative diagram in my note, and it fully autonomously generate the tikzcd diagram. I haven't written any tickzcd code by hand in the past year.
Ladys and gentleman, category theory is solved, by ✨AI✨

2026-02-10 00:27:34 UTC

- reply

There is an ocaml gradescope library https://github.com/qcfu-bu/gradescope_ocaml/ assuming this is what you are looking for.

2026-01-28 01:01:10 UTC

- reply

But what does the fox say?

2026-01-02 22:41:06 UTC

Spend $500 on RAM so that I can open three electron app on a zoom call.

2026-01-02 12:35:04 UTC

- reply

Hey Prof. Jacob, it seems like I cannot access the paper from this URL, can you double check if the URL is correct?

2025-09-20 20:20:11 UTC

unlike donut-shaped donut or mug-shaped mug, donut-shaped mug is neither homoemorphic to donut nor mug.
https://media.mathstodon.xyz/media_attachments/files/115/238/476/906/686/792/original/b917f74a12aec777.jpg

2025-08-28 23:02:15 UTC

Who call them "categories" when "monoid-oids" is right there?!

2025-08-26 14:13:01 UTC

- reply

I feel there are two notions of "languages" here: the first is tooling and the second is foundation.
While the tooling to understand semantics have rapidly modernized in the recent several decades, the foundation is still the same.
This means that you can recover the classical domain literature by specializing modern ones, establishing these connections.
However, a lot of the theorem within Haskell often arises from an idealized fragment, since the full semantics of any industrial programming language is just intractable to reason about within one's mind. Yet, such idealized fragment is never formalized in mathematics. I think this is akin to the idea in https://math.andrej.com/2016/08/06/hask-is-not-a-category/
So, I feel trying to establish connections with coding-focused paper necessarily need to sacrifice formality in order to recover the idealized fragment the original author have in their mind, since again, the full semantics of Haskell is too gigantic, and clearly out of scope for most papers.

2025-08-22 12:56:45 UTC

We should make a new version of Lean using Bool instead of Prop, and call it Boolean.

2025-08-20 10:50:21 UTC

I think there needs to be a category of PL works named "SMT and prayers".

2025-08-15 08:37:24 UTC

If all road leads to Rome, all road also leads to anywhere else with a road.

2025-08-11 19:34:32 UTC

- reply

Indeed the weakest part of my papers are always my research.

2025-07-26 07:31:44 UTC

My research stands between theory and practice.
That means I get to suck at both programming and math.

2025-07-25 18:33:07 UTC

Got some Prolog today with @npub1v6a…c7s4
https://media.mathstodon.xyz/media_attachments/files/114/915/303/746/939/356/original/67e2a2b705781acd.jpg
https://media.mathstodon.xyz/media_attachments/files/114/915/304/235/479/053/original/6f6430b46489571f.jpg

2025-07-02 13:40:48 UTC

Nowadays, the primary drive for my researches is to publish papers with puns in their titles.

2025-06-15 16:00:04 UTC

(• − •)
https://media.mathstodon.xyz/media_attachments/files/114/688/205/268/636/865/original/abee30ae3ae3bb9f.png

2025-06-14 11:35:55 UTC

Math is the only kind of magic where peeking behind the curtain only makes it more fun.

2025-06-09 15:00:27 UTC

Showering is probably the most important invention for scientific advancement.

2025-06-07 19:33:57 UTC

"I am not perfect... I am perfectoid."

2025-05-27 08:54:05 UTC

Data flow is the worst thing that has ever happened to control flow.

2025-02-22 18:22:43 UTC

Bun made it very clear that they are "NOT AVALIABLE"
https://media.mathstodon.xyz/media_attachments/files/114/048/929/814/481/890/original/355eaa4a7bdcc261.jpg

2025-02-17 21:31:49 UTC

Should we build more parks or parking?
https://media.mathstodon.xyz/media_attachments/files/114/021/361/804/207/183/original/25ad3991264d383f.jpeg

2024-11-20 08:16:34 UTC

Contrary to popular American belief, fallen leaves don't bite if you don't point a noisy, smelly, polluting air gun at them.
It is also okay to let grass grow taller than 5cm.
https://media.mathstodon.xyz/media_attachments/files/113/514/288/856/438/823/original/7bb9bf595adf2888.jpg
https://media.mathstodon.xyz/media_attachments/files/113/514/289/070/618/575/original/3d56ace89a856e10.jpg

2024-10-31 22:15:07 UTC

Breaking News! Great Britain just invented Tater tots!
https://media.mathstodon.xyz/media_attachments/files/113/404/327/943/098/334/original/eba503ee38c79f2d.jpg

2024-10-13 15:32:57 UTC

- reply

There is a reason to my madness. As I am planning on leaving the U.S. for my postdoc. I am making some sauces that will help my wife cook.
I was planning garlic sauce (for stir fry), spicy chicken stew base (烧鸡公底料, despite its name, can do almost all spicy stew, and even some stir fry), and chard chili sauce (go into cold dish and can be eaten straight with rice or noodles).
Now, in the light of my 5lb garlic purchase, I have garlic sauce, garlicky spicy stew, and garlic chard chili sauce. Fortunately, my wife really really likes garlic 🤪.
https://media.mathstodon.xyz/media_attachments/files/113/300/835/582/206/341/original/fbaeb850ff68eed7.jpg

2024-10-12 21:49:54 UTC

After having a laugh at @npub1f20…d5dd 's 5lb of New Mexico pepper with my wife, I, in my infinite wisdom, brought 5lb of raw peeled garlic.
https://media.mathstodon.xyz/media_attachments/files/113/296/657/193/132/797/original/4520d0d711981dc8.jpg

2024-10-04 00:41:21 UTC

- reply

Pfff, almost forgot the most important one...
https://media.mathstodon.xyz/media_attachments/files/113/246/370/570/981/643/original/823cdaea57241039.jpg

2024-10-04 00:26:21 UTC

rate my setup
https://media.mathstodon.xyz/media_attachments/files/113/246/311/512/266/309/original/10e57e36dff08ddc.jpg

2024-09-29 14:04:34 UTC

DO **MORE** NIGHTMARKET!
https://media.mathstodon.xyz/media_attachments/files/113/221/216/786/570/366/original/1fd06a24605fb26a.jpg
https://media.mathstodon.xyz/media_attachments/files/113/221/216/942/037/274/original/41b4fb4c8c4567ee.jpg
https://media.mathstodon.xyz/media_attachments/files/113/221/217/118/189/819/original/abf1020d43a2def5.jpg
https://media.mathstodon.xyz/media_attachments/files/113/221/217/275/304/974/original/f68da4207c12cf23.jpg

2024-09-18 15:49:20 UTC

I currently have a plain text single page website (https://czhang03.github.io/). I used to enjoy the plain-text aesthetic, but recently I started to feel that the page is getting too cluttered and do not draw people in anymore.
Should I keep plain text, or do whatever hip CSS thing that people use?

2024-08-15 00:35:55 UTC

Not too bad for a initial sticker bomb
https://media.mathstodon.xyz/media_attachments/files/112/963/233/651/720/286/original/4016ce578a9f8f6a.jpg

2024-08-02 20:31:21 UTC

Do I sticker bomb my laptop