inaseer

Super happy to see Coyote publicly released. Our team within Azure has used it on a number of services and cannot say enough good things about it. It has allowed us to develop code knowing that safety and liveness violations due to subtle race conditions are caught in testing and design time instead of production! For folks familiar with software verification tools, you might know the project as P#. Coyote is an evolution of P# and adds support for testing task-based programming (.NET's TPL framework) in addition to the state-machine based actor programming model.

P# team at Microsoft | Redmond, WA | Contract | Onsite

The P# team at Microsoft works on enabling developers to write reliable, well-designed and well-tested software through model checking and language integration techniques. The approach is reminiscent of TLA+ like techniques but differs in that the code _is_ the model and developers don't have to write models separate from the implementation. P# explores interesting paths through the state space a program can take and produces reproducible traces which can be used to debug and fix issues in services and distributed systems.

This position will involve a variety of tasks including writing samples and documentation to help P# gain wider adoption, and porting parts of the testing infrastructure to work on .NET core. It will also involve working on novel visualization techniques to aid debugging and comprehension of services and distributed systems.

The Banana and Elevator demos did not specify/verify temporal properties so I suspect it doesn't support specifying temporal formulas at the moment (the T in TLA+). This means it can be used to check correctness properties but not liveness properties. Despite this limitation I believe this is a fantastic tool as it makes writing specs way more approachable.

I'm reserving my judgement on the system. Just sharing a few videos which might help in understanding Urbit better. Start with this LamdaConf talk: https://www.youtube.com/watch?v=I94qbWBGsDs and pair with this demo video after: https://www.youtube.com/watch?v=Tp9aCEfA6ao

Types are invaluable when refactoring your code. I have found Typescript to be invaluable when doing exploratory programming as it allows me to refactor heavily as I learn more about the structure of the problem. The compiler points all the affected code sites and I have reasonable confidence in the correctness of the code after the refactor.

Ah, your landing page should make that abundantly clear. That's a very cool feature.

I tried a couple of articles on Washington Post and the algorithm did a decent job. I then read the gist first before reading an article, and while some sentences were a little hard to understand w/o the surrounding context, I felt I still got a decent summary. I can see myself skimming the article through this service instead of relying solely on my eye balls when scanning through.

Couple of suggestions:

- Linking the extracted sentences back to the original page if I want the surrounding context - A tool/browser plug-in which can allow me to select a representative sentence from the story and submit to gist

Seems like a useful stand alone service as it is; having people vote on and submit gists themselves would be cherry on top.

The web is a big place. What's the strategy around seeding it with useful gists so it can gain critical mass? Have you thought about focusing on a niche (say, TED talks?) or possibly automatically summarizing pages? The latter could be tricky as incorrectly or poorly summarized pages would detract users from the site.

I see several relevant results in Bing including the wikipedia entry for Up as the fourth result.