July 3, 2026

America at 250

Yesterday, on my way to the YMCA for my 1700-meter swim, AC on high in 100-degree (“heat dome” over 163 million people across central and eastern US), I was chatting about the story of Freon—invention, then ban.

Freon was invented for air conditioning in 1930 in Dayton, Ohio. The goal was to find a safe, non-toxic replacement for the dangerous refrigerants of the time, such as ammonia and sulfur dioxide. The compound was later known as Freon-12 or CFC-12. It quickly led to the widespread adoption of safe and efficient air conditioning, in vehicles and homes and businesses across the country and then the world.

In 1972, U.S. chemist Rowland at a conference heard the detection of CFC-11 in the air over the Atlantic. This sparked his curiosity: if these human-made chemicals were accumulating in the atmosphere, what ultimately happened to them? Working with his post-doc Molina, they knew CFCs, including Freon, were designed to be inert and non-soluble, meaning they wouldn’t break down in the lower atmosphere through rain or common chemical reactions. The only fate was to drift slowly up to the stratosphere, where intense ultraviolet light would break them apart, releasing highly reactive chlorine atoms. Their model showed a single chlorine atom could act as a catalyst, destroying tens of thousands of ozone molecules in a chain reaction.

The journal Nature published their paper on June 28, 1974. In September, they held a press conference to share their results, initiating advocacy for policy change. Over the next few years, their theory was confirmed by U.S. scientists, institutions and equipment. In 1975, National Oceanic and Atmospheric Administration (NOAA) used air samples collected by weather balloons at heights up to 17.4 miles and found that CFCs were reaching the stratosphere in the predicted amounts and were being broken down at the expected altitudes. NASA Jet Propulsion Laboratory used high-altitude U-2 spy planes and weather balloons to measure hydrochloric acid in the stratosphere and found higher concentrations at higher altitudes (a source of chlorine), which aligned perfectly with the Molina-Rowland theory.

In October 1978, NASA launched Nimbus-7 satellite to carry equipment specifically designed to measure ozone: the Total Ozone Mapping Spectrometer (TOMS). It was groundbreaking because it could create daily global maps of total ozone, giving a bird’s-eye view of the ozone layer worldwide. When the British Antarctic Survey published in 1985 showing unexpectedly low ozone over Antarctica, the Nimbus-7 data became an essential independent check. In fact, TOMS recorded extremely low ozone values in 1983 and 1984, but the values were so far outside the expected range that the computer system flagged them as errors and filtered them out as “bad data.” After the British discovery was published, NASA scientists reviewed the archived TOMS data, reprocessed it without the erroneous low-value filter, and confirmed the findings. The satellite data showed that the dramatic thinning of the ozone layer over the Antarctic had been roughly the size of the United States.

In 1987, in response to the growing scientific consensus, 46 countries signed the Montreal Protocol on Substances that Deplete the Ozone Layer. This treaty is legally binding for phasing out the production and use of CFCs. It was later strengthened with a stricter and faster timeline. The production and import of new Freon was banned in the U.S. and other developed nations starting in 1996, and the developing countries were given time till 2010. China officially stopped the production of CFCs in July 2007 and ended consumption in January 2008, 2.5 years ahead of the schedule.

The 2025 Antarctic ozone hole was the fifth smallest since 1992. Since peaking around 2000, levels of ozone-depleting chlorine in the Antarctic stratosphere have dropped by about a third. The ozone layer is on track to recover to pre-1980s levels by around 2050. Full recovery of the ozone hole over Antarctica is projected for the late 2060s.

250 years of people, innovation, and leadership. That’s worth remembering. Happy Birthday, America.

May 1, 2026

University of Rochester Takes Lean Kernel Arena Top Spot

Lean Kernel Leaderboard

The Lean Kernel Arena (arena.lean-lang.org) is a public benchmarking and testing ground for different proof checkers (kernels) used in the Lean Theorem Prover. It runs a large suite of tests to check the correctness of each checker and reports their speed (⏱️) and memory usage (🧠), especially on large, real-world tests like mathlib (the comprehensive Lean mathematical library). Below is a screenshot of the leaderboard taken on April 29, 2026.

The public ranking includes the official kernels alongside community alternatives based on nanoda (implemented in Rust), lean4lean (written in Lean itself), and rpylean (using just-in-time compiled Python). My PhD student, Yifan Zhu, and I began discussing cache optimization for nanoda a week ago. By Monday morning of this week, Yifan’s version of nanoda had reached the top spot! The techniques he used will be the subject of an upcoming technical report. In this blog, I am merely reporting the numbers, with some context for readers who may not be familiar with Lean.

The leaderboard reports performance in total time, computed by dividing the total instruction count by a clock frequency. The instruction count does not consider the effect of caching. In addition, in multi-threaded kernels, the end-to-end time may be reduced significantly from parallelization. Yifan’s version shows only a 4% reduction in reported time, but in wall-clock time, it is substantially faster. On the benchmark machine running four threads, the wall-clock times are 4.9 minutes for Yifan’s kernel, 6.3 minutes for the second fastest, and 22 minutes for the official version. His Lean kernel is 22% faster than the second‑fastest kernel on the list.

Lean Applications

  • Formalizing mathematics. Lean has been used to formalize mathematical proofs, from undergraduate topics (calculus, linear algebra) to ongoing research. An April 2026 analysis counted over 308,000 declarations, 8.4 million logical connections, and almost 1.4 million lines of Lean code.
  • AI: Groups like Google DeepMind (with its AlphaProof system) use Mathlib as a benchmark and a knowledge base. AI models are trained on Mathlib’s data to learn how to reason and prove theorems automatically.

The most computationally demanding use cases are in the field of artificial intelligence, where AI models require generating and checking millions of potential proof steps. A faster kernel directly reduces the time and energy required to train and run these AI models. Beyond training AI, even standard automated proof tactics, e.g., simp (simplify) repeatedly applying rewriting rules to a goal, rely on kernel speed. With the rise of AI coding agents, the ability to quickly verify AI-generated code is crucial. An experimental AI agent was able to generate a 7,400-line verified embedded DSL over a single weekend, requiring the kernel to check thousands of lines of code for correctness on the fly (slides).

In industrial applications, speed is not just about cost-efficiency but about integrating verification directly into the development workflow. For example, AWS uses Lean to verify its Cedar policy system, ensuring no version ships unless all proofs pass. Microsoft uses Lean to verify its SymCrypt cryptographic library.

C++ vs Rust

I downloaded and counted the number of source lines in two kernels. The first is from https://github.com/leanprover/lean4.git in its src/kernel, counted using cloc:

This second is from https://github.com/ammkrn/nanoda_lib.git:

In reported measures, the official C++ kernels take 30 to 40 minutes and use over 9 GB of memory. The Rust-based kernels, in contrast, take as little as 16.1 minutes in Yifan’s version and use half as much memory. In parallel (4-thread) executions, the wall-clock time is 22 minutes for the official version, compared to 4.9 and 6.3 minutes for the top two Rust-implemented kernels. The parallel speedup, computed by the ratio of the reported time to the wall-clock time, is less than 2× for the C++ kernels and 3.3× for Yifan’s kernel. Overall, the Rust kernels execute fewer instructions and achieve greater parallel efficiency than their C++ counterparts.

* Corrected 5/12/2026: the time reported by the arena website is computed from the total instruction count, not based on measured CPU time.

April 27, 2026

Miss Ratio Monotonicity and Convexity (Part 1)

Caches are dynamically managed local memories. Their dynamic behavior can either improve performance or, in some cases, become detrimental and counterproductive. Monotonicity and convexity are two properties are most commonly used to determine whether a cache design is well‑behaved and provides predictable performance. This is the first of a series blog posts on these properties.

Miss Ratio Monotonicity

Informally:

  • If you increase the cache size, the miss ratio never increases.
  • In other words, the miss ratio is a non‑increasing function of cache size.

Formally:
Let mr(c) be the miss ratio for a cache of size c (measured in blocks). Then for c_1 < c_2, we have mr(c_1) \ge mr(c_2).

Not all caches behave this way. If a cache algorithm is not monotonic, increasing cache size could sometimes increase misses, which is counterintuitive and undesirable. This is known as the Belady’s anomaly.

Stack Algorithms and the Inclusion Property

A caching algorithm has the inclusion property (or is a stack algorithm) if:

For any memory address reference sequence and at any time, the set of blocks in a cache of size c is a subset of the set in a cache of size c+1. Cache contents are inclusive across sizes. A block present in the smaller cache is always present in any larger cache. Therefore, the miss ratio of any stack algorithm is guaranteed non-increasing when increasing the cache size.

Mattson et al. Presented the stack property as the sufficient condition for one-pass evaluation of a caching algorithm. The Stack Simulation maintains the content of all cache sizes at each moment using a stack. At each access, the stack distance is the position of the stack where the accessed data is found. The stack distance fully determines whether the data access is a cache hit or miss.

After stack simulation, the hit or miss count of any cache size can be determined from the stack distances without re‑running the trace. Hence, the paper is titled Evaluation techniques for storage hierarchies.

The classic paper in 1970 established formally that the stack property is a sufficient condition for monotonic miss ratios, and the practical solution of one-pass evaluation. This classic work has been extended later in several ways.

LRU caches are the most important and commonly studied. For example, program locality analysis usually assumes LRU caches. The LRU stack distance shows the “closeness” of data reuse and is often abbreviated as the reuse distance. Stack simulation is too slow for large traces. Much faster algorithms have been developed. See a later blog devoted to studies of reuse distance.

Caching techniques that guarantee monotonic miss ratios:

  • Mattson et al. IBM 1970: LRU, OPT, MRU, LFU, and RR (statistically equivalent to RAND)
    • OPT is optimal for all cache sizes, while the technique for a single cache size is called Belady or MIN
  • Gu and Ding, ISMM 2011: LRU-MRU, used for collaborative caching with binary hints, i.e., the evict-me bit.
  • Gu and Ding, ISMM 2012: priority hints, Priority LRU, and non-uniform inclusion.

The term “stack distance” is often used without specifying which type. All stack algorithms above have their stack distance.

Caching techniques that are not guaranteed to have monotonic miss ratios:

  • Belady, CACM 1969: FIFO
  • Mattson et al. IBM 1970: RAND

As explained in Mattson et al., non-monotonic miss ratios may happen if caching priorities depend on the capacity of the cache and differ from one capacity to another, for example, priorities depending on the frequency of reference to pages after their entering the cache. Another example is when priorities depend on total time spent in the cache.

Summary

Miss ratio monotonicity means larger cache → same or lower miss ratio
Inclusion property ensures miss ratio monotonicity and allows for single-pass evaluation, i.e., you can compute miss ratio curve (MRC) for all cache sizes from one trace run.

April 12, 2026

Programming Language Skills Are AI Skills

Because of AI, everyone needs to know programming languages

Jesen Huang in 2025

Jensen Huang famously said that with modern AI, the programming language becomes human language. Indeed, what used to take days to craft a program, AI tools can now write in seconds. Reports from the industry indicate that many senior engineers have not written a single line of code in months. However, AI coding is directed and managed by humans, and AI-generated code must be approved by humans. Code is cheap, but good code is not. In fact, more AI-generated code often means more human work. A compelling real-world example is the recent Anthropic source code leak, which highlights the risks associated with AI-assisted coding.

Fred Brooks in 1986

In his seminal article that laid the foundation for the field of software engineering, Frederick Brooks identified four essential difficulties of software development. He evaluated the solutions available at the time and concluded that while they addressed accidental difficulties, no solution could resolve the essential ones. He titled his article No Silver Bullet. The introduction begins:

Of all the monsters who fill the nightmares of our folklore, none terrify more than werewolves, because they transform unexpectedly from the familiar into horrors. For these, one seeks bullets of silver that can magically lay them to rest.

I imagine that Anthropic was probably horrified when their AI-generated system leaked over half a million lines of internal source code—a transformation from familiar tool to unexpected nightmare. Brook’s article is the required reading for the first week of the class I have been teaching. The first homework asks students to imagine talking to Jensen Huang and answering his question: “So, what are the essential difficulties of software?”

Programs Require Human Approval

Michael Scott, my colleague and the author of the popular textbook Programming Language Pragmatics, often quotes Donald Knuth: “Programming is the art of telling another human being what one wants the computer to do.” Part of this insight is that a program is a specification for a machine. In this regard, the key attribute is that a program must be precise. We should not—and must not—allow unspecified behavior by a machine. Think about programs that run laser eye surgeries, operate radiation machines, land jetliners, and control the ignition sequence to send Artemis II to the moon. We must write programs that are complete and precise.

AI has an unprecedented ability to automate programming, and its capabilities continue to improve. However, humans must be there to inspect and approve the generated code. The KPMG survey in Q3 2025 found that 63% of 130 executives said they are “putting humans in the loop due to a lack of trust, up from 45% last quarter.” In discussing the survey, one commenter explained that if people do not fully understand what a generated system does and why, they cannot defend it—not to a regulator, not to a client, and not to their leadership.

Precision is the foundation of reasoning. In mathematics, complete precision allows us to derive a result across a hundred steps while still knowing exactly what we are doing—and it enables someone to check every step along the way, a task that machines can now perform. Precision is the foundation of modern science and engineering. We can build complex systems today because we make every component fully precise.

The Conclusion: Everyone Needs to Know Programming Languages

With AI, modern programming may consist of three steps: (1) prompt AI to write code, (2) ensure the code is correct, and (3) explain to another human being what the code does and why it is correct. If Jensen Huang is correct that everyone will program using natural language, then it actually requires that everyone must know programming languages—because step (1) is fraught with risks without steps (2) and (3). Everyone needs to know programming languages enough to understand the code that they write using AI.

March 21, 2026

Software Design and AI-assisted Development Course in Fall 2026

Announced to undergraduate students in an email on March 18, 2026:

Updated for Fall’26

CSC253 Software Design and AI-assisted Development

Software design is a critical discipline because modern software systems are too complex for any single individual to fully comprehend, yet they must be designed to avoid causing harm to the people they serve. This course focuses on the collaborative construction of software by teams. The curriculum covers:

  1. Design Principles and Practices: Information hiding, software architectures, work assignments, team organization, iterative development, and documentation.
  2. Safe Programming in Rust: Generics and traits, ownership and borrowing rules, safe pointers, modules, and design patterns.
  3. AI Assistance: automated code and test generation, specialization, and coordination by coding agents.
  4. Ethical Principles: Fairness and human fallibility.

Assignments emphasize teamwork in software design and development. Students enrolled in CSC 453 are also required to learn Rust meta-programming.

Prerequisites:

  • CSC 172 (Data Structures and Algorithms) or equivalent for CSC 253.
  • CSC 172 and CSC 252 (Computer Organization) or equivalent for CSC 453.

Rust-related industry news:

Example uses:

  • A simple to-do list that runs entirely in a browser, written in either C or Rust using WASM SQLite. The following table compares the two choices. The complete code and commands are generated by DeepSeek (AI) here: https://chat.deepseek.com/share/wkgbopveuwb8cp1xsh
February 22, 2026

Reflection on the Meaning of Charity

This week, billions of people, 1.4 in mainland China, are enjoying their longest holiday of the year. It is a tradition time to reflect, mark an entry in this juncture in time, and share with others. With that spirit, here are my thoughts on the fifth day of the Year of Horse.

A recurring theme in traditional Chinese drama is the contrast between those who help others in urgent need and those who only add to the wealth of the rich. This sentiment appears in the book Slapping the Table in Astonishment (Part One), published around 1627—roughly 200 years after Zheng He’s ocean voyages. The original text reads:

“世间人周急者少，继富者多。为此，达者便说：’只有锦上添花，那得雪中送炭？’ 只这两句话，道尽世人情态。”

This translates to: “In this world, few help those in desperate need, while many add to the fortunes of the already wealthy. Thus, the wise observe: ‘There are always those who gild the lily, but who brings charcoal in the snow?’ These words capture the true nature of human relationships.”

The idea of helping others—going out on a snowy night to deliver firewood to those without heat—once defined my understanding of charity. Before coming to Rochester, I believed that was exactly what charity meant: helping others. Living in Rochester, however, my perspective has changed.

Rochester has a rich legacy. In 1960s and 70s, the “Nifty Fifty” stocks are a group of high-growth, large-cap stocks popular with institutional investors and widely regarded as “one-decision”, that is, buy and never sell. Three of these are in Rochester: Kodak, Xerox, and Bausch & Lomb. George Eastman, who founded Kodak, had a wealth of $100 million (2 billion today) and gave most of it away: $50 million to University of Rochester including Eastman music school and $20 million to MIT (anonymously as Mr. Smith). In his late years, he suffered from a health condition which was extremely painful. After touring the new River Campus of University of Rochester, accompanied by then university president Rush Rhees, he returned home and committed suicide, leaving a brief note: “To my friends: my work is done. Why wait? G.E.”

Rochester is cited as the birthplace of the modern United Way movement. “Checking a box” on a payroll deduction form to donate and support the community is a direct descendant of this tradition. If just visiting, one would not see a difference, but living here for decades, I know how unusual for a city to have a deeply ingrained culture of giving back. Since around 2010, a few years after our second child was born, my family has been donating the equivalent of one dollar per person per day to United Way. In 2025, approximately 50,000 people donated about $16.7 million to this organization alone. The funds are used to support programs run by local charitable organizations. Many people, including us, also donate directly to these groups. I know people who volunteer in these programs. For example, one of our children’s music teacher and her husband volunteer one day each week doing cleaning work at Ronald McDonald House. The picturesque house sits by the canal and a short distance from the UR Hospital, with 24 private bedrooms to house terminally ill children, at no cost to their families. I feel fortunate to be able to donate to United Way and support volunteers who help others. But this is still not the whole meaning of charity.

Today I saw a passage by Vincent van Gogh, who wrote in 1882 to his brother Theo Van Gogh (who supported him through his life and died only 6 months after Vincent died).

What am I in the eyes of most people — a nonentity, an eccentric, or an unpleasant person — somebody who has no position in society and will never have; in short, the lowest of the low. All right, then — even if that were absolutely true, then I should one day like to show by my work what such an eccentric, such a nobody, has in his heart. That is my ambition, based less on resentment than on love in spite of everything, based more on a feeling of serenity than on passion. Though I am often in the depths of misery, there is still calmness, pure harmony and music inside me. I see paintings or drawings in the poorest cottages, in the dirtiest corners. And my mind is driven towards these things with an irresistible momentum. I’m seeking. I’m driving. I’m in it with all my heart. What would life be if we had no courage to attempt anything. (based on translation used by @soulxsigh on TikTok)

Here is what charity truly means: It is not only about helping others—it is also about allowing ourselves to be inspired. Whether it is someone enduring a cold winter night without heat, someone donating their time to lift others up, or someone uncompromisingly charting their own life path, we draw inspiration from them. And we will not be the only ones who find new strength and meaning in their example. A life well lived is one filled with moments of inspiration. In this light, our charity is simply investing our wealth to live a better life—first and foremost for ourselves.

Below is van Gogh’s painting titled Landscape with a Carriage and a Train, with a horse in the center (Source: https://en.wikipedia.org/wiki/Landscape_with_a_Carriage_and_a_Train). Wishing everyone a happy time in the Year of the Horse. 马到成功 (Mǎ dào chéng gōng) — may you succeed in arriving.

Fun fact: In 2020, Rochester United Way received a record $35 million donations. The unusual total is due to the historic $20 million gift from MacKenzie Scott.

November 7, 2025

CSC 579 Logic Foundation and Machine-Checked Proofs

CSC 579 Spring 2026
(R 9:40am to 10:55 Wegmans 1005)

The language of intelligence is logic. The course teaches proof systems, with a focus on Coq. You will learn to use Coq to formalize logic, which is the fundamental language of rational thought and problem-solving, and construct sound and verifiable proofs. A similar system, Lean 4, was used by generative AI, Alpha Proof, to solve Olympiad-level math problems. By learning the fundamentals of modern proof systems, you acquire a complete foundation for logical thinking and the knowledge and skill to use or build automated reasoning systems.

Pre-requisites: Students enrolling in the course are expected to have advanced knowledge in either programming languages (CSC 253, 254 or 255), math, or logic.

Syllabus

  • The Need for Training Thought: The Values of Thought. Tendencies Needing Constant Regulation.  Regulation Transforms Inference into Proof.
  • Type Systems.  Operational Semantics. Progress. Type Preservation. Type Soundness.
  • Functional Programming in Coq: Data and Functions.  Proof by Simplification, Rewriting and Case Analysis.
  • Proof by Induction. Proofs Within Proofs.  Formal vs. Informal Proof.
  • Lists, Options, Partial Maps.
  • Basic Tactics: apply, apply with, injection, discriminate, unfold, destruct.
  • Logic in Coq. Logical Connectives: Conjunction, Disjunction, Falsehood and Negation, Truth, Logical Equivalence, Logical Equivalence, Existential Quantification.  Programming with Propositions. Applying Theorems to Arguments. Coq vs. Set Theory: Functional Extensionality, Propositions vs. Booleans, Classical vs. Constructive Logic.
  • Inductively Defined Propositions. Induction Principles for Propositions.  Induction Over an Inductively Defined Set and an Inductively Defined Proposition.
  • The Curry-Howard Correspondence. Natural Deduction. Typed Lambda Calculus. Proof Scripts. Quantifiers, Implications, Functions. Logical Connectives as Inductive Types.

Textbooks

Related Industry News

October 25, 2025

In Memoriam: Professor Tang, Shiwei (唐世渭) of PKU

Professor Tang was my undergraduate thesis advisor three decades ago. He passed away on Tuesday. Below is the English translation of the main passages of the article on Thursday in China’s Guangming Daily, full text in Chinese at https://mp.weixin.qq.com/s/JzjPkV0MMUjhlfibbRLNyw

Professor Tang Shiwei was born in December 1939 in Ningbo, Zhejiang Province. He graduated from the Computational Mathematics program of the Department of Mathematics and Mechanics at Peking University in 1964 and remained at the university to teach after graduation. He was promoted to professor in August 1990 and retired in December 2004.

Professor Tang Shiwei was a founder of the database as an academic discipline in China. He long dedicated himself to teaching and research in databases and information systems. He served as Director of the Database Research Laboratory in the Department of Computer Science and Technology at Peking University, Director of the Peking University Computing Center, Director of the Information Science Center, Director of the National Key Laboratory of Visual and Auditory Information Processing, Vice Chair of the Database Professional Committee of the China Computer Federation, and Professional Advisor to the Beijing Municipal People’s Government, making significant contributions to the development of computer science research and education in China.

At Peking University, he spearheaded the development of China’s independently copyrighted database management system, COBASE and the domestic system software platform COSA, for which COBASE was a key component and received a national award in 1996.

Original text in Chinese by Jin Haotian (晋浩天), correspondent, Guangming Daily

I took the database class around 1993, taught by his colleague Professor Yang, Dongqing (杨东清) and then joined their research group for my undergraduate thesis. I remember Professor Tang mentioning to me that they were the first in China to learn the development of databases in the US including reading the source code of early database systems. As a student assistant, I was sent to visit the Bank of China and talk to to account operators. It was pretty much deaf-mute conversation — I knew the textbook but nothing about applications let alone banking, but at the time I thought I was there to tell them what to do. Later a senior graduate student went to redo the visit. I was given part of the consulting fee even though my contribution might have been negative. Professor Tang was most generous and encouraging to me. I am fortunate and proud to be a part of his legacy.

Professor Tang also directed the undergrad thesis of Yuanyuan Zhou, now a professor at UCSD.

May 26, 2025

2025 CS Commencement Welcome

3:00 PM, May 17, 2025 | BAAC Auditorium

Dear Colleagues, parents, guests, and most important, our graduates:

Welcome to the 2025 CS graduation ceremony. I’m the department chair Professor Chen Ding.

Our 150 bachelor graduates and 30 MS graduates, here and elsewhere, you make today special: not just the day of graduation, but also the day we graduate the largest class in the department’s 50-year history.

At a commencement 20 years ago, David Foster Wallace told a parable: Two young fish swimming along, and they happen to meet an older fish swimming the other way, who nods at them and says, ‘Morning. How’s the water?’ And the two young fish swim on for a bit. Then one looks at the other and asks, ‘What is water?’

Parables are open to interpretation. So what is water the pervasive medium shaping our life? It is tech and increasingly CS. Computing principles drive every aspect from hardware to software to application. Blockchain, quantum computing, and autonomous driving all emerged from CS research. According U.S. Labor Statistics, over 60% of STEM jobs require CS skills. CS is transformative in other fields too. In this class, 96 undergrads, or almost two-thirds, took another major or minor.

Before going for his PhD, a student of mine plans to traverse the Continental Divide from El Paso, Texas, to Banff, Canada. Let his journey be not a symbol but embodiment of the grueling work of learning you did in the past and the daunting uncertainty of future you may be facing now.

Marcus Arellius said: Impediment to action advances action. Think 2700 miles, on a bike, alone, and camping under open skies. What stands in the way, becomes the way. Every challenge and setback is not blocking your path. It is the path. Our muscles strengthen, and our brain forms strong neural path ways when we work through our difficulties, none when things are easy.

You have done the hard work. What is the future?

CS is the engine of innovation. So much we have today did not exist even last year. This SSD card, a stamp in size, not much thicker, stores 1TB data. A question for parents and guests: raise your hand if you have used ChatGPT? An open-source equivalent is DeepSeek. You can download its data. The full model is 1TB. Most things we ask on Google you can now ask on ChatGPT or DeepSeek. Hence, information equivalent to Google Search is literally at my fingertip.

The power is immense majestic and terrifying. We see increasing inequality and political polarization at home, conflicts and wars abroad. CS is not innocent. Do you realize that we are the last generation who lived before social media? This little card tokenizes either human knowledge with unlimited potential or an existential threat, the ultimate FOOBAR.

This brings me to my final point, a last lesson if you will. A principle I teach in collaborative software design is that we are all fallible. Software is designed by people for people. Moral and human questions are infinitely more complex than math and science. There is no logical or mathematical certainty. The truth depends on a balance between two sets of conflicting reasons. It is crucial that you listen to people with whom you disagree, so you can go through the same mental journey they took to their conclusion. Quoting JS Mill: “In the human mind, one-sidedness has always been the rule, and many-sidedness the exception. Therefore, open our minds to listen to our opponents, thank them to do for us that otherwise we ought to do for ourselves.

To recap, everyone is fallible. We approach truth best by working together.

Speaking on behalf of all faculty and staff, congratulations. We will watch you with joy and pride. And we will always be here when you return to visit.

February 16, 2025

CSC 253 Collaborative Software Design Rate My Professor Chen Ding Fall 2024

Anonymous inputs were collected by the university before the final exam. 17 out of 24 students (71%) submitted the evaluation.The overall Instructor Rating is 4.53, and the overall Course Rating 4.44.

Two anonymous comments:

  • Professor Ding is a great professor and a strong proponent of Rust. Taking his class has introduced me to many benefits of Rust and broadened my horizon on collaborative programming, software design, and software testing. I believe acquiring these knowledge is beneficial for me and my teammates (it goes both ways) on the long run.
  • The final DVCS group project workload is very imbalanced and hard to control. Some group members even disappeared during the last half of the project.


Related posts: