hwayne/lets-prove-leftpad
View on GitHub ↗ ★ 758 SystemVerilog
Proving leftpad correct two-dozen different ways
9 mentions on Hacker News by 6 people: 4 stories, 5 comments · first 2020-02-14 · latest 2025-11-03
20082026
-
…[1] http://concrete-semantics.org [2] https://github.com/lean-forward/logical_verification_2025 [3] https://github.com/hwayne/lets-prove-leftpad
comment by nextos · 2025-11-03 · in Why don't you use dependent types? -
…you want to use String and StringBuilder to do the padding, which arguably be more idiomatic. [1] https://github.com/hwayne/lets-prove-leftpad/blob/ea9c0f09a2... [2] https://docs.oracle.com/en/java/javase/25/docs/api//java.bas... [3]…
comment by marginalia_nu · 2025-10-15 · in Breaking "provably correct" Leftpad -
▲ 2
Let's Prove Leftpadstory by asplake · 2025-10-07 · 1 comment
-
▲ 2
Proving leftpad correct two-dozen different waysstory by nequo · 2024-06-12 · 0 comments
-
…of proofs of leftpad in different prover languages, so people can compare them. It's here: https://github.com/hwayne/lets-prove-leftpad [/invalid closing tag]
comment by hwayne · 2024-06-12 · in Terence Tao on proof checkers and AI programs -
…Haskell community" My experience is that other refinement type systems are way less complex. See: https://github.com/hwayne/lets-prove-leftpad In particular, compare https://github.com/hwayne/lets-prove-leftpad/blob/master/liq... to…
comment by nextos · 2022-10-16 · in Simon Peyton Jones interview -
▲ 2
Let's Prove Leftpadstory by nextos · 2021-10-02 · 0 comments
-
▲ 1
Let’s Prove Leftpad (Comparing proof tools)story by mbrodersen · 2021-06-24 · 0 comments
-
…code correct via inline JML annotations. [1]: https://amturing.acm.org/vp/clarke_1167964.cfm [2]: https://github.com/hwayne/lets-prove-leftpad
comment by hwayne · 2020-02-14 · in The Business Case for Formal Methods