News for hackers. Stuff that matters.
Re:Functional Programming in C++ (2013) by mlitchard on Saturday July 25, 2015 @02:23PM (#9948477)
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.
Re:Functional Programming in C++ (2013) by varelse on Saturday July 25, 2015 @02:35PM (#9948519)
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.
Re:Functional Programming in C++ (2013) by mlitchard on Saturday July 25, 2015 @05:07PM (#9949018)
It's not a problem for you, but it's a problem generally. That's why so many people are working to solve it.