4 ms·

>but they've already been around for ages and didn't yet revolutionise the world of software design. I think it's mostly because languages with dependent types

>but they've already been around for ages and didn't yet revolutionise the world of software design. I think it's mostly because languages with dependent types are awfully clunky to use. Perhaps dependent typing is even a dead end, but I wouldn't count out other ideas such as refinement typing just yet. I think it will take a lot of work and failed attempts (such as typestate in early Rust) to get fancy type theory into mainstream languages (just like it took a while for Java to get lambdas). Case in point: static analysis tools for C++ are getting more capable and popular recently.

krapht 7y ago
Formal methods in general are extremely clunky to use. Just see how much hate Rust gets for making it extremely difficult to make an intrusive linked list. And memory safety is only one kind of correctness assertion. So I'm gonna be a pessimist here and say: nope, not gonna be the future, because programmers are lazy and "ship it now" is better than "prove the bugs don't exist".
- yakshaving_jgt 7y ago
  Not all programmers build WordPress plugins. Some programmers write software for aircraft. The "ship it now" maxim doesn't exist in that context.
  - onion2k 7y ago
    Unless it's Boeing.
  - lonelappde 7y ago
    No one is writing aircraft software in Haskell. They need good control over memory usage.
    - Legogris 7y ago
      Counter-example: https://smaccmpilot.org/software/index.html https://smaccmpilot.org/software/index.html Also, a Haskell DSL for automotive control systems: http://tomahawkins.org/ http://tomahawkins.org/
      - krapht 7y ago
        That isn't a counter-example unless you're taking his post literally. In which case I claim that Python is a system programming language because one time somebody somewhere wrote a driver in it.
- AnimalMuppet 7y ago
  Well... for 95-99%[1] of all software being written, "ship it now" beats "prove that bugs don't exist". Better formal methods could really help that 1-5%, but they're not going to impact the 95% very much. [1] All statistics made up on the spot. I think it's in the right ballpark, though.
UncleMeat 7y ago
The cpp static analysis tools are all wildly unsound. This is a core design principle behind all real world deployable static analysis systems, whether they are based on abstract interpretation or model checking or symbolic execution, or anything else. Static analysis is a powerful technique. But sound formal methods have been failing to make a splash for nearly five decades.
- antisemiotic 7y ago
  Honestly, I'd be happy with a language that can propagate the result of a conditional statement into compile-time constraints inside the branches, and also can create executables without jumping through 20 hoops.

krapht 7y ago

Formal methods in general are extremely clunky to use. Just see how much hate Rust gets for making it extremely difficult to make an intrusive linked list. And memory safety is only one kind of correctness assertion. So I'm gonna be a pessimist here and say: nope, not gonna be the future, because programmers are lazy and "ship it now" is better than "prove the bugs don't exist".

yakshaving_jgt 7y ago
Not all programmers build WordPress plugins. Some programmers write software for aircraft. The "ship it now" maxim doesn't exist in that context.
- onion2k 7y ago
  Unless it's Boeing.
- lonelappde 7y ago
  No one is writing aircraft software in Haskell. They need good control over memory usage.
  - Legogris 7y ago
    Counter-example: https://smaccmpilot.org/software/index.html https://smaccmpilot.org/software/index.html Also, a Haskell DSL for automotive control systems: http://tomahawkins.org/ http://tomahawkins.org/
    - krapht 7y ago
      That isn't a counter-example unless you're taking his post literally. In which case I claim that Python is a system programming language because one time somebody somewhere wrote a driver in it.
AnimalMuppet 7y ago
Well... for 95-99%[1] of all software being written, "ship it now" beats "prove that bugs don't exist". Better formal methods could really help that 1-5%, but they're not going to impact the 95% very much. [1] All statistics made up on the spot. I think it's in the right ballpark, though.

UncleMeat 7y ago

The cpp static analysis tools are all wildly unsound. This is a core design principle behind all real world deployable static analysis systems, whether they are based on abstract interpretation or model checking or symbolic execution, or anything else. Static analysis is a powerful technique. But sound formal methods have been failing to make a splash for nearly five decades.

antisemiotic 7y ago
Honestly, I'd be happy with a language that can propagate the result of a conditional statement into compile-time constraints inside the branches, and also can create executables without jumping through 20 hoops.