4 ms·

There is already finite element analysis. It basically works on arbitrarily complex structures their internal connections, loads, etc. (It enabled the current b

by pas 7y ago

There is already finite element analysis. It basically works on arbitrarily complex structures their internal connections, loads, etc. (It enabled the current boom in super skinny high rises and various fancy structures.) We don't really have that for programming, but it's not like we shouldn't try. (Eg we have TLA+ for processes, we can use Coq and others for proving some parts of programs.)

naasking 7y ago
> We don't really have that for programming, but it's not like we shouldn't try. We do in the form of abstract interpretation and various other global static analyses. Unfortunately, these analyses are non-compositional, where small code changes can lead to dramatic and unpredictable long-range effects in the properties of your code. Finite-element analysis has similar non-compositional properties. A type system is a compositional form of static analysis, and composition obviously has considerable reuse and cost reduction benefits, which is probably why most programming doesn't use static analysis tools beyond type systems.
- pas 7y ago
  Finite-element analysis - as far as I know - has the advantage of being able to estimate its own errors with some practically useful local upper bound. Because physics at that level is very much local. (Though it can't really help with higher level problems, like cyclic dynamical load and resonance problems, but there are other tools for that.) > [...] most programming doesn't use static analysis tools beyond type systems. Yes, unfortunately. :( It'd be great to have access to much better/stricter tools to be able to check just some interesting/important parts of programs (eg. pure business logic modules/functions) without resorting to reimplementing them in static-analysis systems.
  - naasking 7y ago
    LiquidHaskell!

4 ms·

There is already finite element analysis. It basically works on arbitrarily complex structures their internal connections, loads, etc. (It enabled the current b

by pas 7y ago

naasking 7y ago
> We don't really have that for programming, but it's not like we shouldn't try. We do in the form of abstract interpretation and various other global static analyses. Unfortunately, these analyses are non-compositional, where small code changes can lead to dramatic and unpredictable long-range effects in the properties of your code. Finite-element analysis has similar non-compositional properties. A type system is a compositional form of static analysis, and composition obviously has considerable reuse and cost reduction benefits, which is probably why most programming doesn't use static analysis tools beyond type systems.
- pas 7y ago
  Finite-element analysis - as far as I know - has the advantage of being able to estimate its own errors with some practically useful local upper bound. Because physics at that level is very much local. (Though it can't really help with higher level problems, like cyclic dynamical load and resonance problems, but there are other tools for that.) > [...] most programming doesn't use static analysis tools beyond type systems. Yes, unfortunately. :( It'd be great to have access to much better/stricter tools to be able to check just some interesting/important parts of programs (eg. pure business logic modules/functions) without resorting to reimplementing them in static-analysis systems.
  - naasking 7y ago
    LiquidHaskell!