3 ms·
Languages I'd like to write: * a language with a mix of contracts and refinement types: encoding preconditions and postconditions in types of input and output
by krcz 8y ago
Languages I'd like to write:
* a language with a mix of contracts and refinement types: encoding preconditions and postconditions in types of input and output values. this way one can match postconditions of one function and precodnitions of the next. but programmer wouln't have to prove everything: the checks could be run-time or disabled overall, enabled just for testing, which could replace unit tests - asserting all conditions for example inputs would be enough,
* a language with possibility of restricting computational model per subroutine. not everything requires Turing completeness. orthogonally, most functions can be pure. the goal would be to stick to simpler models if you can and only use more complex one in small part of the codebase,
* a language with possibility of user defined linear types (/ affine types / relevant types), e.g. make it possible to require having every exception logged as an error, unless explicitly ignored,
* a language designed to be translated into other languages with the translation being readable code (in contrast to CLJS, ScalaJs, etc.), as idiomatic as possible; e.g. translating map / filter chains to loops when translating to imperative language.
This might be as well one language, but as complexity rises exponentially, it might be better to start with few smaller ones instead.
- ellius 8y agoLove bullet #2. Being able to start with more constrained features and using more powerful techniques when necessary would be a huge aid in developing good architectures.
- krcz 8y agoIn such case I highly recommend Noether: Symmetry in Programming Language Design presentation by Daira Hopwood: https://www.infoq.com/presentations/noether https://www.infoq.com/presentations/noether. It explores the idea by describing a possible stack of sublanguages ranked from simple and easy to reason about to complex and robust.
- nn3 8y agoDon't we already have that to some degree in GNU C? gcc has an __attribute__((pure)) (not sure if it enforces it though) and there are C++ constexprs.
- np_tedious 8y agoI think it's a compiler hint for optimizations, but the onus of correctness (ie. Is this really pure) remains on the programmer / whatever generates the C code
- klntsky 7y ago> the checks could be run-time or disabled overall, enabled just for testing If you do not require proofs, how is that different from C-like asserts and unit testing? How are refinement types related?
- krcz 7y agoyou could have mix of assertions and proofs, obtaining something that you could call gradual verification - you wouldn't have to prove everything from axioms, you could base on assertions. the difference from asserts and unit testing is that you could match post-contract from one function with pre-contract of another one, as in: fun sort(l: List[Int]): SortedList[Int] fun minusReverse(l: SortedList[Int]): SortedList[Int] = l.map(el => -el) fun f(l: List[Int]): SortedList[Int] = minusReverse(sort(l)) when you have sort and minusReverse functions unit-tested, you could use proof system to prove that f is correct (assuming that sort and minusReverse are). while looking for similar concepts in existing programming languages I have found that SPARK 2014 [1] (subset of Ada 2012 with static verification) follows such philosophy: you can prove some parts of the code and unit test the rest. [1] https://www.adacore.com/about-spark https://www.adacore.com/about-spark [2] http://docs.adacore.com/spark2014-docs/html/lrm/introduction.html#combining-formal-verification-and-testing http://docs.adacore.com/spark2014-docs/html/lrm/introduction...