9 ms·

AI, machine learning, and neural networks are, of courwe, booming, but I consider them to be hyped. I consider type theory and formal verification to be more p

by meuk 8y ago

AI, machine learning, and neural networks are, of courwe, booming, but I consider them to be hyped. I consider type theory and formal verification to be more promising (but more academic). Distributed systems and everything having to do with parallel and/or high-performance systems is a good midway between what the industry likes and what's interesting from an academic point of view.

bitL 8y ago
Funny, distributed systems supervisors often warn their students that there is a huge disconnect between theory and practice and if they really want to be in the field.
- jrumbut 8y ago
  I was amazed when I took a distributed systems class what exists or is known about but is almost never used. Still, an expert there is probably pretty industry friendly, and someone somewhere must have a distributed objects/CORBA system that can't be dismantled.
Davidbrcz 8y ago
Haha. Formal verification has been around for 40/50 years and we can't say it is a wide success from a industrial point of view. It has some achievements in terms of results/methods and projects checked, but on a daily basis, pretty much no one uses it. We are ages away of having every programmer understanding formal verification and having all programs verified/proved. Type theory is in a similar situation. Many issues in code could be solved with basic typing algorithms but people and companies favor languages with poor/no typing (python, Javascript).
- rhizome31 8y ago
  Not so long ago the same could be said about AI.
  - xyproto 8y ago
    And perpetual energy! Guess we, as humans, just aren't great at predicting the future, regardless of what the last 50 years looked like.
- whatshisface 8y ago
  Rust looks like a step towards practical formal verification just because of its design philosophy. I think what we're doing is making engineering languages more and more verifiable as research languages become more and more expressive. Eventually they'll meet in the middle and we'll have formal verification in "real life."
  - amelius 8y ago
    Yes, but: https://news.ycombinator.com/item?id=16442743 https://news.ycombinator.com/item?id=16442743
  - adrianN 8y ago
    No progress in language theory can fix the fundamental problem of software verification: you need a formal specification to have anything to verify. Who wants to write not only a detailed spec for their code, but a spec that has well defined semantics in some kind of logic? Nobody, that's who. There are very few properties that you care about that are both sufficiently easy to encode in a formal specification and not provided automatically by a safe language.
    - whatshisface 8y ago
      In the logical extreme that can't be the case, because a fully debugged program plus a machine to run it on actually satisfy the definition of a formal specification. Deciding what you want your program to do is the eternal burden of programming, but maybe there's a way to make formal specification at least as easy as regular programming.
      - adrianN 8y ago
        But then you already have a perfect implementation that you somehow made without the use of formal verification. But you want to introduce formal verification because translating real-world requirements into a formal language is hard enough that you can't be sure of correctness...
    - joe_the_user 8y ago
- jacoblambda 8y ago
  The biggest barrier to adoption of formal verification that I have seen as someone just starting in the field (working through Software Foundations and have a number of projects planned with SPARK, Frama-C, and LiquidHaskell) is the lack of groundwork. Verifying just your own code is complex enough as it is but working with libraries without any clear specification of their interfaces and behaviours makes this so much harder. I think there is real value in having verified libraries or at least libraries with well defined specs so that interfacing with other code wasn't so tedious. I think this issue is starting to be overcome with regard to the usage of strong type systems. Truly strongly typed languages are finally getting the libraries and communities built up so that they don't seem quite as daunting.
  - deleted 8y ago
    [deleted]
  - bor0 8y ago
    To me, personally, the biggest barrier was lack of a proper introduction with a lot of examples. I try to break this barrier a bit with my upcoming book: Gentle Introduction to Dependent Types with Idris. I am very interested in this area but it is impossible for newcomers to get a grasp of it without too much digging. Logical Foundations was OK but I was still missing the theoretical explanation ("why does this tactic work? it is magic!"). So with accumulated knowledge from IRC, forums I hope to address this.
    - jacoblambda 8y ago
      Ooh I'll check this book out once I get through the pile of stuff I have right now. And as you noted there definitely is a lot of "magic" when it comes to the inner workings of theorem proving tactics. I'm slowly figuring all of that out but like you said it definitely takes time and digging at the moment.
    - hackermailman 8y ago
      The Little Typer is out soon too https://mitpress.mit.edu/books/little-typer https://mitpress.mit.edu/books/little-typer
- denzil_correa 8y ago
  > Formal verification has been around for 40/50 years and we can't say it is a wide success from a industrial point of view. It has some achievements in terms of results/methods and projects checked, but on a daily basis, pretty much no one uses it. Formal verification is an essential part of mission critical applications. Therefore, even though they might be few in number - their impact is pretty significant and "wide".
  - incadenza 8y ago
    That’s interesting you say that. I’ve known two engineers who worked at JPL and they said that no teams did anything close to formal verification. It’s an incredibly difficult bar to meet
    - Davidbrcz 8y ago
      She/He is right and I was a bit cynical in my answer. There are some real industrial projects that used formal methods. I have in mind Airbus with ASTREEE, the Meteor subway system (Paris' subway line 14), Windows' drivers with the SLAM analyzer... Also, JPL released its model-checker Java PathFinder and hosts every year the Nasa Formal Method conference so I'm pretty confident that at least someone at NASA is interested in formal methods =)
- Shoue 8y ago
  We're definitely moving in the direction. Someone already mentioned Rust, and Typescript is gaining traction in web dev. Banks like Barclays and Standard Chartered already have Haskell teams, and I've noticed more and more Haskell jobs popping up over the years (in London). Scala is already realtively popular. Formal verification is used in some niche areas (BAE, Galois). Proof Engineer is a real role some companies are looking to fill.
- dorfsmay 8y ago
  Machine learning has been around with no success from an industrial point of view until very recently. Until fairly recently, nobody cared and few understood big O notation. Recent prog languages have added syntax to avoid issues such as "off by on error" (generator etc...), TDD is slowly becoming a standard everywhere. The next step to improve quality in software is formal verification IMO. There is quite a bit of research in that domain and even some academic program languages integrating it within their syntax.
- gchadwick 8y ago
  > but on a daily basis, pretty much no one uses it. Maybe not for software but certainly in the hardware world formal verification is common place with mature tools available from multiple vendors.
- meuk 8y ago
  You're absolutely right, and that's exactly why I am enthusiastic about these fields. I think there is a ton of potential, and that these fields will be booming once the industry discovers this. Of course, the point is not to prove every program correct. But it should be feasible to prove security-critical parts correct, especially for large companies. The biggest problem is that formal verification is about as un-sexy as it gets, since it has no applications an sich.

by meuk 8y ago

bitL 8y ago

Funny, distributed systems supervisors often warn their students that there is a huge disconnect between theory and practice and if they really want to be in the field.

jrumbut 8y ago
I was amazed when I took a distributed systems class what exists or is known about but is almost never used. Still, an expert there is probably pretty industry friendly, and someone somewhere must have a distributed objects/CORBA system that can't be dismantled.

Davidbrcz 8y ago

Haha. Formal verification has been around for 40/50 years and we can't say it is a wide success from a industrial point of view. It has some achievements in terms of results/methods and projects checked, but on a daily basis, pretty much no one uses it. We are ages away of having every programmer understanding formal verification and having all programs verified/proved. Type theory is in a similar situation. Many issues in code could be solved with basic typing algorithms but people and companies favor languages with poor/no typing (python, Javascript).

rhizome31 8y ago
Not so long ago the same could be said about AI.
- xyproto 8y ago
  And perpetual energy! Guess we, as humans, just aren't great at predicting the future, regardless of what the last 50 years looked like.
whatshisface 8y ago
Rust looks like a step towards practical formal verification just because of its design philosophy. I think what we're doing is making engineering languages more and more verifiable as research languages become more and more expressive. Eventually they'll meet in the middle and we'll have formal verification in "real life."
- amelius 8y ago
  Yes, but: https://news.ycombinator.com/item?id=16442743 https://news.ycombinator.com/item?id=16442743
- adrianN 8y ago
  No progress in language theory can fix the fundamental problem of software verification: you need a formal specification to have anything to verify. Who wants to write not only a detailed spec for their code, but a spec that has well defined semantics in some kind of logic? Nobody, that's who. There are very few properties that you care about that are both sufficiently easy to encode in a formal specification and not provided automatically by a safe language.
  - whatshisface 8y ago
    In the logical extreme that can't be the case, because a fully debugged program plus a machine to run it on actually satisfy the definition of a formal specification. Deciding what you want your program to do is the eternal burden of programming, but maybe there's a way to make formal specification at least as easy as regular programming.
    - adrianN 8y ago
      But then you already have a perfect implementation that you somehow made without the use of formal verification. But you want to introduce formal verification because translating real-world requirements into a formal language is hard enough that you can't be sure of correctness...
  - joe_the_user 8y ago
jacoblambda 8y ago
The biggest barrier to adoption of formal verification that I have seen as someone just starting in the field (working through Software Foundations and have a number of projects planned with SPARK, Frama-C, and LiquidHaskell) is the lack of groundwork. Verifying just your own code is complex enough as it is but working with libraries without any clear specification of their interfaces and behaviours makes this so much harder. I think there is real value in having verified libraries or at least libraries with well defined specs so that interfacing with other code wasn't so tedious. I think this issue is starting to be overcome with regard to the usage of strong type systems. Truly strongly typed languages are finally getting the libraries and communities built up so that they don't seem quite as daunting.
- deleted 8y ago
  [deleted]
- bor0 8y ago
  To me, personally, the biggest barrier was lack of a proper introduction with a lot of examples. I try to break this barrier a bit with my upcoming book: Gentle Introduction to Dependent Types with Idris. I am very interested in this area but it is impossible for newcomers to get a grasp of it without too much digging. Logical Foundations was OK but I was still missing the theoretical explanation ("why does this tactic work? it is magic!"). So with accumulated knowledge from IRC, forums I hope to address this.
  - jacoblambda 8y ago
    Ooh I'll check this book out once I get through the pile of stuff I have right now. And as you noted there definitely is a lot of "magic" when it comes to the inner workings of theorem proving tactics. I'm slowly figuring all of that out but like you said it definitely takes time and digging at the moment.
  - hackermailman 8y ago
    The Little Typer is out soon too https://mitpress.mit.edu/books/little-typer https://mitpress.mit.edu/books/little-typer
denzil_correa 8y ago
> Formal verification has been around for 40/50 years and we can't say it is a wide success from a industrial point of view. It has some achievements in terms of results/methods and projects checked, but on a daily basis, pretty much no one uses it. Formal verification is an essential part of mission critical applications. Therefore, even though they might be few in number - their impact is pretty significant and "wide".
- incadenza 8y ago
  That’s interesting you say that. I’ve known two engineers who worked at JPL and they said that no teams did anything close to formal verification. It’s an incredibly difficult bar to meet
  - Davidbrcz 8y ago
    She/He is right and I was a bit cynical in my answer. There are some real industrial projects that used formal methods. I have in mind Airbus with ASTREEE, the Meteor subway system (Paris' subway line 14), Windows' drivers with the SLAM analyzer... Also, JPL released its model-checker Java PathFinder and hosts every year the Nasa Formal Method conference so I'm pretty confident that at least someone at NASA is interested in formal methods =)
Shoue 8y ago
We're definitely moving in the direction. Someone already mentioned Rust, and Typescript is gaining traction in web dev. Banks like Barclays and Standard Chartered already have Haskell teams, and I've noticed more and more Haskell jobs popping up over the years (in London). Scala is already realtively popular. Formal verification is used in some niche areas (BAE, Galois). Proof Engineer is a real role some companies are looking to fill.
dorfsmay 8y ago
Machine learning has been around with no success from an industrial point of view until very recently. Until fairly recently, nobody cared and few understood big O notation. Recent prog languages have added syntax to avoid issues such as "off by on error" (generator etc...), TDD is slowly becoming a standard everywhere. The next step to improve quality in software is formal verification IMO. There is quite a bit of research in that domain and even some academic program languages integrating it within their syntax.
gchadwick 8y ago
> but on a daily basis, pretty much no one uses it. Maybe not for software but certainly in the hardware world formal verification is common place with mature tools available from multiple vendors.
meuk 8y ago
You're absolutely right, and that's exactly why I am enthusiastic about these fields. I think there is a ton of potential, and that these fields will be booming once the industry discovers this. Of course, the point is not to prove every program correct. But it should be feasible to prove security-critical parts correct, especially for large companies. The biggest problem is that formal verification is about as un-sexy as it gets, since it has no applications an sich.