5 ms·

it's always nice to see some real-world ada. however, this reimplementation appears to have not ported over one crucial feature of the original: conciseness.

by 5- 5y ago

it's always nice to see some real-world ada. however, this reimplementation appears to have not ported over one crucial feature of the original: conciseness. (this, however, might just be due to the host language; this is also why i only admire ada from a distance).

MaxBarraclough 5y ago
Conciseness isn't a virtue in itself. It's only ever a virtue in so far as it aids readability/maintainability/writability/etc. The approach here is, presumably, to get the code absolutely right the first time, then leave it alone forever. It doesn't need to be easy to change. Also, Ada makes a conscious decision to favour readability over writability, the idea being that code is read many more times than it is written. It does so by being verbose and making quite heavy use of keywords rather than symbols. Opinions vary on whether it succeeds in improving readability.
- touisteur 5y ago
  Well to be precise, the approach is to write the spec once, and optimize the shit out of the implementation, whilst keeping proof as a safeguard.
  - touisteur 5y ago
    Although... Not sure about the constant-time or stack-size guarantees, if they're necessary here, which spark doesn't support (for now?).
    - MaxBarraclough 5y ago
      I'm not an expert in SPARK but I believe stack-size bounds can be determined using the GNATstack static-analysis tool. [0] I imagine it's difficult to formally prove that a program is invulnerable to timing attacks. I believe even branch-free machine code isn't necessarily safe, as modern CPUs are clever and complex creatures. [0] https://www.adacore.com/gnatpro/toolsuite/gnatstack https://www.adacore.com/gnatpro/toolsuite/gnatstack
      - MaxBarraclough 5y ago
        Can confirm GNATstack is appropriate for use with SPARK: https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#dealing-with-storage-error https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...
        touisteur 5y ago
        Yes gnatstack is neat, but, last time I tried (which was some time ago, I'll admit) there were some quite big limits and caveats with gnatstack analysis. The un precise analysis on second-stack, dynamic-sized object return, pointer-access calls (the last one being forbidden in spark?), and some others were quite blocking for my use cases.
        MaxBarraclough 5y ago
        Makes sense. The analysis will be downright impossible if you permit everything. Calls to arbitrary function pointers, or OOP dynamic-dispatch, for instance (unless these can be fully accounted for). I imagine it works well if you use MISRA C, which forbids function pointers. It looks like SPARK doesn't forbid function pointers, [0] although it bans plenty else. [1] I wonder if that's an issue for GNATstack. GNATstack is presumably mostly aimed at safety-critical code, as software in most other domains will be satisfied just relying on testing. Presumably, such codebases are likely to be using constrained language subsets anyway. [0] https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html#subprogram-pointers https://docs.adacore.com/spark2014-docs/html/ug/en/source/ac... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/source/language_restrictions.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/la...
        touisteur 5y ago
        Thanks for digging. I get there'd be limitations but I would prefer sometimes consistency: for gnatstack to support at least the SPARK subset (so, OOP, access to procedures, most 'reasonable' provable language features). I'm not faulting AdaCore, just noting the slight inconsistency, as I was disappointed first back then. I think it's a worthy space to improve though, because it's happened to me, on AoRTE (silver-level) SPARK, to crash because of an overeager parser. Fuzzing and more formal testing helps smoke some of those out but I'd like AoRTE to mean AoRTE :-) at least in no-dynamic-allocation-so-'new'-can't-fail scenarios. I'm guessing it's mostly 'no-one put a wad of cash thick enough on the table to have another look' which is understandable. I'll probably try to hit some corporate trouser pockets to start the engine again :-)
deleted 5y ago
[deleted]

by 5- 5y ago

MaxBarraclough 5y ago

Conciseness isn't a virtue in itself. It's only ever a virtue in so far as it aids readability/maintainability/writability/etc. The approach here is, presumably, to get the code absolutely right the first time, then leave it alone forever. It doesn't need to be easy to change. Also, Ada makes a conscious decision to favour readability over writability, the idea being that code is read many more times than it is written. It does so by being verbose and making quite heavy use of keywords rather than symbols. Opinions vary on whether it succeeds in improving readability.

touisteur 5y ago
Well to be precise, the approach is to write the spec once, and optimize the shit out of the implementation, whilst keeping proof as a safeguard.
- touisteur 5y ago
  Although... Not sure about the constant-time or stack-size guarantees, if they're necessary here, which spark doesn't support (for now?).
  - MaxBarraclough 5y ago
    I'm not an expert in SPARK but I believe stack-size bounds can be determined using the GNATstack static-analysis tool. [0] I imagine it's difficult to formally prove that a program is invulnerable to timing attacks. I believe even branch-free machine code isn't necessarily safe, as modern CPUs are clever and complex creatures. [0] https://www.adacore.com/gnatpro/toolsuite/gnatstack https://www.adacore.com/gnatpro/toolsuite/gnatstack
    - MaxBarraclough 5y ago
      Can confirm GNATstack is appropriate for use with SPARK: https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html#dealing-with-storage-error https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...
      - touisteur 5y ago
        Yes gnatstack is neat, but, last time I tried (which was some time ago, I'll admit) there were some quite big limits and caveats with gnatstack analysis. The un precise analysis on second-stack, dynamic-sized object return, pointer-access calls (the last one being forbidden in spark?), and some others were quite blocking for my use cases.
        MaxBarraclough 5y ago
        Makes sense. The analysis will be downright impossible if you permit everything. Calls to arbitrary function pointers, or OOP dynamic-dispatch, for instance (unless these can be fully accounted for). I imagine it works well if you use MISRA C, which forbids function pointers. It looks like SPARK doesn't forbid function pointers, [0] although it bans plenty else. [1] I wonder if that's an issue for GNATstack. GNATstack is presumably mostly aimed at safety-critical code, as software in most other domains will be satisfied just relying on testing. Presumably, such codebases are likely to be using constrained language subsets anyway. [0] https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html#subprogram-pointers https://docs.adacore.com/spark2014-docs/html/ug/en/source/ac... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/source/language_restrictions.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/la...
        touisteur 5y ago
        Thanks for digging. I get there'd be limitations but I would prefer sometimes consistency: for gnatstack to support at least the SPARK subset (so, OOP, access to procedures, most 'reasonable' provable language features). I'm not faulting AdaCore, just noting the slight inconsistency, as I was disappointed first back then. I think it's a worthy space to improve though, because it's happened to me, on AoRTE (silver-level) SPARK, to crash because of an overeager parser. Fuzzing and more formal testing helps smoke some of those out but I'd like AoRTE to mean AoRTE :-) at least in no-dynamic-allocation-so-'new'-can't-fail scenarios. I'm guessing it's mostly 'no-one put a wad of cash thick enough on the table to have another look' which is understandable. I'll probably try to hit some corporate trouser pockets to start the engine again :-)

deleted 5y ago

[deleted]