Conversation

Oct 20, 2017

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!

Quote Tweet

Jonathan Edwards

@jonathoda

· Oct 20, 2017

Docs-as-apps will be a big thing. Been my target for long. Latest entrant: Coda blog.coda.io/its-a-new-day- Wonder how deep they went?

Show this thread

what's missing with contemporary type theories? a proper treatment of holes!

Craig Stuntz

@craigstuntz

Oct 20, 2017

I had an interesting discussion with another developer last week. He noted it annoys him when projects are configured to run a linter...

Craig Stuntz

@craigstuntz

Oct 20, 2017

...before the test suite. His point is that when doing TDD he wants to hack together a "correct" solution before a "pretty" one. But...

Craig Stuntz

@craigstuntz

Oct 20, 2017

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...

Craig Stuntz

@craigstuntz

Oct 20, 2017

about type holes. It strikes me that, generally speaking, there are certain types of static analysis we want to do before other types.

Craig Stuntz

@craigstuntz

Oct 20, 2017

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...

Craig Stuntz

@craigstuntz

Oct 20, 2017

AFTER test execution but before deployment" or something. Not sure of the full picture.

@edwinb@types.pl

@edwinbrady

Oct 20, 2017

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.

Replying to

and

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.

8:22 PM · Oct 20, 2017Twitter Web Client