lets-prove-leftpad

> there is not anything necessarily wrong with dependent types, but that he doesn't believe they are necessary. I think that, at least in software engineering, his point has not been disproven. Isabelle (classical) has a great track record in software verification. I don't see it as something inherently inferior to Rocq (dependently typed), which also has a great track record. Lean doesn't have a great focus (yet?) on software verification. And Agda is also not mainstream on large-scale industrial verification. One interesting thing would be to compare Concrete Semantics [1] (Isabelle) vs The Hitchhiker's Guide to Logical Verification [2] (an approximate rewrite in Lean). I am still starting with the second one, so I can't say much yet, but it might be too basic to draw any conclusions. Ultimately, refinement types embedded in general-pur

> The leftpad function provided[1] didn’t take a string, but a char[]. Thankfully, it’s easy to convert from String objects, using the .toCharArray() function. So I did that. Java's unicode handling is a monumental footgun of the most devastating variety where it works for most common cases, and almost all code that is not written with care to how it is handled will not deal well with code points that require more than 2 bytes to represent. If you insist on using a char array (which is a bit unidiomatic), you should be using Character$charPointCount[2] to figure out how many code points are in the array, and even then you're probably SOL with regards to non-trivial emojis. String$charPointCount[3] is also an option if you want to use String and StringBuilder to do the padding, which arguably be more idiomatic. [1] https://github.com/hway

[shameless plug]I maintain a collection 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]

It's interesting he discusses Liquid Haskell (proofs via refinement types) extensively: "So, for me, that’s as far as increasing our ability to give you statically guaranteed theorems about Haskell programs. My money’s on Liquid Haskell at the moment and I hope that we the 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 https://github.com/hwayne/lets-prove-leftpad/blob/master/daf... For me this has been a bit of a disappointment.

It's possible to use TLA+ for complex serial systems, and it can def help there. The thing is that TLA+ is designed to be good at modeling concurrent problems, problems that have a lot of specific challenges you don't see in serial systems. So if you know your system is serial and nondeterministic, then you're probably better off with something that focuses on that part of the design space. To paraphrase Edmund Clarke's Turing lecture[1], the problems of verifying software include "floats, strings, user-defined types, procedures, concurrency, generics, storage, libraries…" If you're not worried about verifying concurrency in your tool, you've got a more resources to devote towards verifying the other things. That's also a space I don't have as much familiarity with, so I don't know what the best tools are there. My vague understand is tha