hwayne

47 ms·

541.
by hwayne 8y ago
> UPDATE: The rumor may be completely false because the official 1Password account on Twitter commented: “My humans and I are happily independent and plan to remain so.”
542.
Sketch.systems: Formal Methods for UIs(sketch.systems)
4 points by hwayne 8y ago|0 comments
543.
Are functional programs easier to verify than imperative programs? (2018)(semantic-domain.blogspot.com)
3 points by hwayne 9y ago|0 comments
544.
by hwayne 9y ago
It means I don't understand Prolog very well and really shouldn't have namedropped it :P
545.
by hwayne 9y ago
I don't think I've heard of this before; I'd love to watch it if you have a link!
546.
by hwayne 9y ago
Yeah, it's probably more accurate to say that "everybody from the Algol line used := for assignment", with C being the first language of that line to stop.
547.
by hwayne 9y ago
Here's a PDF about running BCPL on a Raspberry Pi: http://www.cl.cam.ac.uk/~mr10/bcpl4raspi.pdf It's aimed at teaching programming to 10 year olds no prior experience. One of the first examples is implementin
548.
Searching for “Production Hell” at Ford’s Kentucky Truck Plant(dailykanban.com)
2 points by hwayne 9y ago|0 comments
549.
by hwayne 9y ago
Yeah, it's extremely important to note that any correctness technique - tests, types, contracts, formal methods - only provides _more_ confidence, not _complete_ confidence. We have to think of defense-in-depth.
550.
by hwayne 9y ago
You might wanna check out ACL2, which is a theorem prover rooted in common lisp: http://www.cs.utexas.edu/users/moore/acl2/
551.
by hwayne 9y ago
_That said_, I've been making a lot of homemade granola recently. Maybe I should try bringing that next time! Here's a recipe I really like: https://www.epicurious.com/expert-advice/how-to-make-granola...
552.
by hwayne 9y ago
I've used it for caching, batch processing, and concurrent web apps, and it's been a huge help. I've gone into how I used it in a couple of places: - "Tackling Concurrency Bugs with TLA+" ( https://www.you
553.
by hwayne 9y ago
You miss NaN of the shots you don't take
554.
What does VR reveal about the 4th dimension?(albert-hwang.com)
1 points by hwayne 9y ago|0 comments
555.
Monad Tutorials for Other Topics(hillelwayne.com)
2 points by hwayne 9y ago|0 comments
556.
by hwayne 9y ago
Another one I love on the same topic is Peter Gutmann's thesis on formal verification: http://www.cypherpunks.to/%7Epeter/04_verif_techniques.pdf
557.
by hwayne 9y ago
In all honesty it's more a comfort thing: I'm so used to vanilla Python that the extra stuff in Pandas messes with my head. It's just easier for me to work in a completely different language. Also J is more fun as a puzzle la
558.
by hwayne 9y ago
> 1. How do we really get the feel for the benefits of this model? Sure, I can struggle through tutorials on TLA, white papers on Daedalus, and the Eve live demo, but from the little I've seen it's not yet obvious to me how the
559.
by hwayne 9y ago
If you don't mind me tagging in, TLA+ is a specification language, while Haskell is a programming language. You can choose the granularity of states. So if you were trying to implement a Haskell program that took elements of A and outp
560.
by hwayne 9y ago
My first resource on these things is the absolutely fantastic book "Making Software", which has overviews of a lot of these questions how they're studied. The studies they looked at didn't find a correlation between pure
561.
by hwayne 9y ago
> The only thing I disagree with in this article is the leeway given to supposedly legendary programmers who can somehow write bug-free code without tests, specifications, or an inkling of communication with others. I absolutely agree w
562.
by hwayne 9y ago
Thank you! I was heavily inspired by Dan Luu's blog ( https://danluu.com/ ), so I'd recommend checking that out too.
563.
by hwayne 9y ago
TDD is only ~15 years old. Cleanroom and correct-by-construction both have some solid studies supporting them, but take very different approaches than TDD does. They tend to be more rigorous and also take longer so again, it's a case-b
564.
by hwayne 9y ago
It's a bit of a tongue in cheek and a bit of a roast. Eric Smith does TDD consulting.
565.
by hwayne 9y ago
Yeah. "Pure" TDD is strict cycles of "Write failing test, write the bare minimum of code that passes, refactor", which most studies suggest isn't much more helpful than the "common practice" TDD of "w
566.
by hwayne 9y ago
Ron Jeffries' mistake was thinking that he could just use TDD to solve sudoku, as opposed to research and up-front design. Testing does not substitute for thinking.
567.
by hwayne 9y ago
It also left out Alloy, which is another really exciting formal method that a lot of really cool work has been done in.
568.
by hwayne 9y ago
And not just _that_, but TLA+ is really good at expressing liveness conditions, like "the database is EVENTUALLY consistent" or "the algorithm will eventually terminate." Most other formal methods don't cover that.
569.
by hwayne 9y ago
> Liveness having to do with maintaining invariants over the lifetime of a computation. Nit: liveness is about reaching 'good' states over the lifetime of your computation. If your invariant is violated, even if it's a mul
570.
by hwayne 9y ago
I sometimes describe TLA+ to people as "unit-testable flowcharts." It's pretty inaccurate but kinda gets the idea across?

More ›