Objective-Arts
Objective-Arts/lens-dist
相关职业SOC
基于 SOC 职业分类
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
直接命令不会经过审查 Prompt；运行前请先检查来源。
npx skills add https://github.com/Objective-Arts/lens-dist --skill correctness命令会保持在同一行。复制前请横向滚动并检查完整内容。
想先保存到本地？可下载 SkillsMP 当前能够提供的文件。
正在显示 SKILL.md
基于 SOC 职业分类
| name | correctness |
| description | Formal methods |
| allowed-tools | [] |
Edsger Dijkstra's core belief: Programming is a branch of applied mathematics. Programs should be derived from specifications through rigorous reasoning, not hacked together and tested until they seem to work.
"Program testing can be used to show the presence of bugs, but never to show their absence."
Testing finds bugs. It doesn't prove correctness. For critical software, you need mathematical reasoning, not just passing tests.
From his Turing Award lecture (1972):
"We shall do a much better programming job, provided that we approach the task with a full appreciation of its tremendous difficulty, provided that we stick to modest and elegant programming languages, provided that we respect the intrinsic limitations of the human mind and approach the task as Very Humble Programmers."
Our brains are limited. We can only hold so much in working memory. Therefore:
"The competent programmer is fully aware of the strictly limited size of his own skull; therefore he approaches the programming task in full humility."
You are not smart enough to write correct complex programs by intuition. No one is. Use discipline instead.
Dijkstra, with Dahl and Hoare, established structured programming.
"The go to statement as it stands is just too primitive; it is too much an invitation to make a mess of one's program."
The problem with goto: it makes program flow impossible to reason about. You can't look at a statement and know how you got there.
Not this:
start:
read(x)
if x < 0 goto negative
if x > 100 goto toolarge
process(x)
goto start
negative:
print("negative!")
goto start
toolarge:
print("too large!")
goto start
This:
while true:
read(x)
if x < 0:
print("negative!")
elif x > 100:
print("too large!")
else:
process(x)
All programs can be written with only:
No goto needed. Ever.
Structured code has one entry, one exit per block. This makes reasoning possible:
From "A Discipline of Programming":
"We should not ask 'How do we write this program?' but 'How do we derive this program from its specification?'"
The process:
For any statement S and postcondition R, the weakest precondition wp(S, R) is the weakest condition that guarantees R after S executes.
Example:
Statement: x := x + 1
Postcondition: x > 5
wp(x := x + 1, x > 5) = x > 4
If x > 4 before, then x > 5 after.
To prove a loop correct:
Example:
// Invariant: sum = a[0] + a[1] + ... + a[i-1]
sum := 0
i := 0
while i < n:
sum := sum + a[i]
i := i + 1
// Postcondition: sum = a[0] + ... + a[n-1]
The invariant plus i = n (termination) proves the postcondition.
"Simplicity is prerequisite for reliability."
Complex programs cannot be understood. Programs that cannot be understood cannot be trusted. Therefore: simplicity is mandatory.
"Elegance is not a dispensable luxury but a quality that decides between success and failure."
Elegant solutions are:
"In their capacity as a tool, computers will be but a ripple on the surface of our culture. In their capacity as intellectual challenge, they are without precedent in the cultural history of mankind."
Programming is an intellectual discipline. Beauty and elegance are not decorations—they are signs that you've found the right solution.
"The separation of concerns... even if not perfectly possible, is the only available technique for ordering one's thoughts."
Break problems into independent pieces. Solve each piece. Combine solutions.
Each layer should be:
"The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise."
Abstraction isn't hiding complexity. It's creating a level where complexity doesn't exist.
"It is practically impossible to teach good programming to students that have had a prior exposure to BASIC: as potential programmers they are mentally mutilated beyond hope of regeneration."
(Harsh, but his point: bad habits learned early are nearly impossible to unlearn.)
"The tools we use have a profound and devious influence on our thinking habits, and therefore on our thinking abilities."
Choose languages, tools, and practices that encourage rigorous thinking.
"Besides a mathematical inclination, an exceptionally good mastery of one's native tongue is the most vital asset of a competent programmer."
Clarity of thought requires clarity of expression. If you can't explain it clearly, you don't understand it.
From his EWDs (numbered manuscripts):
"The question of whether a computer can think is no more interesting than the question of whether a submarine can swim."
"Computer Science is no more about computers than astronomy is about telescopes."
"Perfecting oneself is as much unlearning as it is learning."
"Simplicity is a great virtue but it requires hard work to achieve it and education to appreciate it. And to make matters worse: complexity sells better."
"If debugging is the process of removing software bugs, then programming must be the process of putting them in."
Before committing code, ask:
Apply these checks:
Dijkstra championed formal methods—mathematical proof of program correctness.
Even without full formal proof:
Use a different skill when:
algorithms (literate programming)design-patterns (23 patterns catalog)java (Effective Java idioms)optimization (profiling, data-oriented)clarity (readability, naming)Dijkstra is the formal methods skill—use it when correctness must be proven, not just tested.
"How do we convince people that in programming simplicity and clarity—in short: what mathematicians call 'elegance'—are not a dispensable luxury, but a crucial matter that decides between success and failure?" — Edsger W. Dijkstra