http://lambda-the-ultimate.org/node/5256
it looks like they reference your work at any rate. 
After these years, what I have learned is that program verification starts
with
program construction. I call this program-first program verification. To
me, dependent
types in themselves are not really a feature for greatly facilitating
program construction
(e.g., we can compare dependent types with OOP, type classes, etc.).
Actually, most
people are likely to find it (much) harder to write programs in a
dependently typed setting :(On Tuesday, September 29, 2015 at 5:28:12 PM UTC-4, Raoul Duke wrote:
Dependent Types for Low-Level Programming | Lambda the Ultimate
it looks like they reference your work at any rate.
Actually, most
people are likely to find it (much) harder to write programs in a
dependently typed setting
This is why things like the Liquid Types research is hopeful to me. I
hope somebody can find ways to make these things more automagical.
(Yes, I know that can bring trouble with it, too.)
As I see it, the problem is not just to have more “automagic”.
People tend to write buggy programs; more automation usually
means more incomprehensible error message reporting.On Friday, October 2, 2015 at 2:11:40 PM UTC-4, Raoul Duke wrote:
Actually, most
people are likely to find it (much) harder to write programs in a
dependently typed settingThis is why things like the Liquid Types research is hopeful to me. I
hope somebody can find ways to make these things more automagical.
(Yes, I know that can bring trouble with it, too.)