NathanCollins

Great point! I have a "cheap" Samsung M32 that I bought for about $170. One reason I chose this Samsung phone over a similarly priced phone from a competitor was that I wrongly believed that Samsung provided several years more OS and security updates. After buying the phone I realized that longer support only applied to flagship models :/

It's not a toggle, but Google Pixel phones (or at least the one I owned a few years ago) come with very few if any bloatware type apps, since the default Android apps are the Google apps anyway. Contrast with Samsung that duplicates a bunch of core apps/functionality.

Are you aware of /The Implementation of Functional Programming Languages/ by Simon Peyton Jones, the main person behind the front end of the GHC Haskell Compiler? The full book is available free on his web site as PDF:

https://www.microsoft.com/en-us/research/publication/the-imp...

It has two chapters on pattern matching, two chapters on type checking, and several chapters related to execution.

I have not read it.

Thanks for clarifying "white-box testing".

Some comments:

* the operations in the mathematical spec are mostly well defined, but e.g. division by zero is not defined. However, the verification handles this by checking that all operations are well-defined on all possible inputs.

* yes, identifying the "edge cases" is not something you can do easily, and hard to make formal. In some sense, the fact the non-edge-case inputs are treated in a uniform way is probably what allows the verification to succeed at all.

* a short summary of the answer you already found in the third blog post: what we actually verify is the LLVM assembly that Clang produces when compiling the C program. Much of the potentially undefined behavior in a C program is translated away by the compiler on the way to LLVM assembly. For any potential undefined behavior that remains in the LLVM assembly, the verification checks that it cannot happen at runtime.

I don't think I understand what you mean by "white-box testing" here, but perhaps it's helpful to clarify what I meant by "equivalence" above, and how it relates to testing: what we did here was verify input/output equivalence between the imperative C code and our functional mathematical spec in Cryptol, for a range of key and input buffer sizes. This corresponds to testing all inputs of those sizes, which is not possible to do by direct testing: e.g., for a 64 byte key and a 1000 byte message, the equivalence corresponds to checking

8^(64 + 1000) =

772229093352564060021182203061704429810699485400692901921197 543030601797302324658889178066005708227773161814337173682980 065612522479316644103460638515687114933331680544961552375412 914711698479251875125441335427310394080188149008724146221306 402242642191159219745353079189135871713826154087180913177991 135554545843425504232155742364801022614341625532175948198587 539576566458760517446126909555225085347521013376171505426231 008775737688282539095967230536510936329489906183630574979494 541005574981802619546120394597788656899688609063922312837993 473534655739423794995816974687759952971465473538229880976237 137410666755636310464327792929854669852851716265627988045993 010404521026728809660275537200281773360887456757531693050082 473180078568595877659952113273156104380151800825339034988199 020562681928372626978536148813617979584497069978086989075685 756621893032191527888867820144068182725496496585643739551119 7590300209437142003442599950379602277911674788208191414992896

tests, which would take "forever" to verify by direct testing.

We did not prove any properties of our mathematical specification in Cryptol, but the claim is that it's close enough to the official FIPS mathematical specification for HMAC [1] that it's easy to believe that it's correct. However, a group at Princeton has also verified HMAC in the past, and gone further than us by not only proving that the imperative C code is input/output equivalent to their mathematical spec in Coq, but also proving that their mathematical spec has the security properties of a secure hash function [2].

[1] http://csrc.nist.gov/publications/fips/fips198-1/FIPS-198-1_...

[2] https://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf

Do you mean as opposed to e.g. verifying the absence of timing attacks? While I agree that verifying the absence timing attacks is probably much harder than what was done here, the difficult part of the s2n verification I linked to was that we verified equivalence between imperative C code and a functional mathematical specification.

Janrain and Engine Yard have been known to host community events.

Yes, this is the only change I care about :( I used "It's All Text" with Emacs. Maybe it's time to start using a separate email client?

In the context of the article, I think the justification was: assuming you're more productive in quality and not quantity, because you're working towards ambitious goals, then on most days you will not complete a recognized goal. The suggestion is to go out of your way to recognize your smaller day-to-day accomplishments which help you reach the big goal.

how do i know you don't suck at making up coding questions?

in other words, why require a sign-up instead of just posting the questions on your site?

E.g. search for "Buck Adams".

Email from prof:

"I need to apologize to everyone in CS 367 for providing data sets containing offensive material. I had not looked at the contents of the large and huge data sets until well after the assignment had been released. Had I realized what the data sets contained, I never would have used them. I am sorry that this happened. "

Full assignment:

http://pages.cs.wisc.edu/~hasti/cs367-common/assignments/p5/...

had not, thanks for the link

there are more important things happening on march 19th:

http://stackin.hauntedshit.com/wp-content/uploads/2009/03/20...

:)

The actual DevHouse Pittsburgh site http://devhousepgh.org is down ...

If you aren't familiar with SuperHappyDevHouse see http://superhappydevhouse.org/.

From http://www.alphalab.org/about.aspx:

    Funding

    Innovation Works will invest $25,000 in each AlphaLab company in
    return for 3% of the common stock of the company. This funding
    should support company operations during the AlphaLab program. As
    Innovation Works utilizes funds from the Commonwealth of
    Pennsylvania, each company receiving funding is expected to
    maintain a significant presence in Pennsylvania after the
    program.

    14) Do we have to stay in Pittsburgh after the program ends?

    Companies are expected to remain in Pittsburgh after the end of the
    AlphaLab program. Our goal is to help you build a successful
    technology company and to add to the critical mass of flourishing tech
    companies in the Pittsburgh region. We believe that Pittsburgh is a
    great place to build a company and after your experience at AlphaLab
    we are confident that you will agree.

I don't get around that much myself, but can add: The AlphaLab office space is on the South Side, which is the big "night life" area, with a bunch of bars, clubs, restaurants, and for some reason a tattoo parlor on every other block (maybe drunk people are more likely to spontaneously get tattoos?). Overall Pittsburgh kind of reminds of Portland, OR, since it's green, cheap, and has a big river (two actually) running through the downtown. It's also supposed to rain a lot like Portland, but that hasn't started yet ...

Yes, I forgot to list this, but it's significant.

* each team gets a one-on-one meeting with the AlphaLab team every week, and when something urgent comes up they can usually make time for another meeting or discuss it on the spot.

* between the AlphaLab program advisors and Innovation Works (the parent company) there are a bunch of experienced business people and entrepreneurs to get advice from and network with.

Together these people have helped us with all sorts of stuff, from developing business documents like executive summaries and seeking further investment to setting up focus groups to test and discuss our product.

I don't have experience with YC's program first hand, but anecdotally AlphaLab blows YC away in terms of amount hands on business help you get. Makes sense when the program only includes six start ups and is backed by a mature investment firm. For teams like ours with a lot of technical experience but very little business experience this seems pretty important.

I'm currently part of the first cycle of this program. AlphaLab has some benefits over YC:

  * includes office space
  * more money for less equity
  * longer program
  * cheaper city to live in

From the article:

"We have a wonderful ability here to choose the right tool for the job. We have components that are written in Java, in C++, in Python, and Ruby and Perl. [Python is] definitely viewed internally here by some of the best computer scientists in the world, people from MITs AI [artificial intelligence] and CS [computer science] labs, as enterprise worthy," he said.

No indication that they're replacing any of the hard core algorithmic stuff that's discussed here:

http://www.paulgraham.com/carl.html