documents, forms, programs will one day be modes of use of the same tool. we're working on that with Hazel. need a solid type theory first!https://twitter.com/jonathoda/status/921436878141784069 …
-
Show this thread
-
what's missing with contemporary type theories? a proper treatment of holes!
2 replies 4 retweets 9 likesShow this thread -
Replying to @neurocy
I had an interesting discussion with another developer last week. He noted it annoys him when projects are configured to run a linter...
1 reply 0 retweets 0 likes -
Replying to @craigstuntz @neurocy
...before the test suite. His point is that when doing TDD he wants to hack together a "correct" solution before a "pretty" one. But...
1 reply 0 retweets 0 likes -
Replying to @craigstuntz @neurocy
One can also use the type system (in some langs!) to show correctness,and type checker usually runs before tests! So that got me thinking...
1 reply 0 retweets 0 likes -
Replying to @craigstuntz @neurocy
about type holes. It strikes me that, generally speaking, there are certain types of static analysis we want to do before other types.
1 reply 0 retweets 0 likes -
Replying to @craigstuntz @neurocy
Ideally the type checker guides you in a sensible path towards correct code, with type holes maybe a mechanism for "stiff I want to check...
1 reply 0 retweets 0 likes -
Replying to @craigstuntz @neurocy
AFTER test execution but before deployment" or something. Not sure of the full picture.
1 reply 0 retweets 0 likes
I've wondered (without much thought yet) if expressive types, plus holes for hard to prove things, would be a good way to generate tests.
-
-
Would love to be able to just shell out to a quickchecky thing instead of having to prove every little thing. Could be good for prototyping.
0 replies 0 retweets 0 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.