3 ms·

Here's the relationship. How can you guarantee your low-level code is correct? Here's one way. You have a language like Idris create a DSL that targets the mach

Here's the relationship. How can you guarantee your low-level code is correct? Here's one way. You have a language like Idris create a DSL that targets the machine you want. You can model what the set of correct programs in your domain look like, and then produce correct code. That's why functional programming in general, and dependent-type programming in particular, is useful for low-level problem domains.

varelse 11y ago
That's not a problem. The application in question was a redesign of an MPI FORTRAN implementation that can produce the same outputs to within FPRE. To verify the low-level code, we just run in double-precision and make sure it matches to 1 part in 10e-9 so across 200+ daily conformance tests. Production mode runs in single-precision with 64-bit Fixed Point accumulation. And that's also been demonstrated to have numerical stability nearly equivalent to running in full double-precision.
- mlitchard 11y ago
  It's not a problem for you, but it's a problem generally. That's why so many people are working to solve it.