3 ms·

Statically checking refinements still only works so-so, that is, what do you do when the SMT solver times out? Writing manual proofs (or proof fragments) is gre

• saosebastiao 9y ago
  I use the Refined library for scala and it works incredibly well (a few bumps here or there, and some occasional boilerplate for library interop). On my app server, it basically becomes my validation layer for all request data, after which I only worry about object ownership/authorization. The big win with refined types is from compiler level support though. With relatively simple checking occurring mostly at IO boundaries, you can eliminate or make obsolete massive portions of testing, type checking, manual optimization, etc., and enable massive amounts of automated optimization. In other words, the "too expensive" refinement checking at runtime becomes a net performance and engineering benefit over the whole product lifecycle.
• floatboth 9y ago
  Runtime refinements are actually useful for places where you'd have checks anyway. E.g. in Haskell, this library http://nikita-volkov.github.io/refined/ http://nikita-volkov.github.io/refined/ — can be integrated with JSON: https://github.com/myfreeweb/magicbane/blob/7c417504590fc40ecd37a61e3c3a80640eb4d8dd/library/Magicbane/Validation.hs https://github.com/myfreeweb/magicbane/blob/7c417504590fc40e... — and you get input validation specified right in the types of your data structures.